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

reconsider A = <*G1,G2,G3*> as multMagma-Family of {1,2,3} ;

A is commutative

reconsider A = <*G1,G2,G3*> as multMagma-Family of {1,2,3} ;

A is commutative

proof

hence
<*G1,G2,G3*> is commutative multMagma-Family of {1,2,3}
; :: thesis: verum
let x be Element of {1,2,3}; :: according to GROUP_7:def 8 :: thesis: A . x is commutative

( x = 1 or x = 2 or x = 3 ) by ENUMSET1:def 1;

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

end;( x = 1 or x = 2 or x = 3 ) by ENUMSET1:def 1;

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