let H be multMagma-Family of 2; :: thesis: ( H = <%G1,G2%> implies ( H is Group-like & H is associative ) )
assume A1: H = <%G1,G2%> ; :: thesis: ( H is Group-like & H is associative )

now :: thesis: for i being set st i in 2 holds
ex Hi being non empty Group-like multMagma st Hi = H . i

let i be set ; :: thesis: ( i in 2 implies ex Hi being non empty Group-like multMagma st Hi = H . i )
assume i in 2 ; :: thesis: ex Hi being non empty Group-like multMagma st Hi = H . i
then ( i = 0 or i = 1 ) by TARSKI:def 2, CARD_1:50;
hence ex Hi being non empty Group-like multMagma st Hi = H . i by A1; :: thesis: verum

end;

hence H is Group-like by GROUP_7:def 3; :: thesis: H is associative

now :: thesis: for i being set st i in 2 holds
ex Hi being non empty associative multMagma st Hi = H . i

let i be set ; :: thesis: ( i in 2 implies ex Hi being non empty associative multMagma st Hi = H . i )
assume i in 2 ; :: thesis: ex Hi being non empty associative multMagma st Hi = H . i
then ( i = 0 or i = 1 ) by TARSKI:def 2, CARD_1:50;
hence ex Hi being non empty associative multMagma st Hi = H . i by A1; :: thesis: verum

end;

hence H is associative by GROUP_7:def 4; :: thesis: verum