Apply unknownprop_9a59ecd7e83aeba0d4be9a32b55c5c57c6083b63a3b259e3f5889e4923a1993d with
abelian_Group_alt,
MagmaHom,
struct_id,
struct_comp leaving 3 subgoals.
The subproof is completed by applying unknownprop_631eb72f9cd6bca41d0746b078fdb35511fad9619f5979579823465a86235144.
The subproof is completed by applying unknownprop_b5511c14c1ee2f1a4f5d54490a6f49a9e3e55efbe1b09846defcd9e57362fad6.
The subproof is completed by applying unknownprop_1790b10b9d586d1da0cc05a071ed8f23b82b55aba45f302d2dcb0a067804bd91.