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

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

A is Group-like

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

A is Group-like

proof

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

( x = 1 or x = 2 ) by TARSKI:def 2;

hence A . x is Group-like by FINSEQ_1:44; :: thesis: verum

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

hence A . x is Group-like by FINSEQ_1:44; :: thesis: verum