let G1, G2 be non empty commutative multMagma ; :: thesis: <*G1,G2*> is commutative multMagma-Family of {1,2}
reconsider A = <*G1,G2*> as multMagma-Family of {1,2} ;
A is commutative

proof

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

end;

hence <*G1,G2*> is commutative multMagma-Family of {1,2} ; :: thesis: verum