let G1 be non empty commutative multMagma ; :: thesis: <*G1*> is commutative multMagma-Family of {1}

reconsider A = <*G1*> as multMagma-Family of {1} ;

A is commutative

reconsider A = <*G1*> as multMagma-Family of {1} ;

A is commutative

proof

hence
<*G1*> is commutative multMagma-Family of {1}
; :: thesis: verum
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;x = 1 by TARSKI:def 1;

hence A . x is commutative by FINSEQ_1:def 8; :: thesis: verum