theorem :: GROUP_7:21

for G1, G2 being commutative Group holds <*G1,G2*> is Group-like associative commutative multMagma-Family of {1,2} ;