let G1 be commutative Group; :: thesis: <*G1*> is Group-like associative commutative multMagma-Family of
reconsider A = <*G1*> as multMagma-Family of ;
A is commutative

proof

let x be Element of {1}; :: according to GROUP_7:def 8 :: thesis: A . x is commutative
x = 1 by TARSKI:def 1;
hence A . x is commutative by FINSEQ_1:def 8; :: thesis: verum

end;

hence <*G1*> is Group-like associative commutative multMagma-Family of ; :: thesis: verum