let G1, G2, G3 be Group; :: thesis: <*G1,G2,G3*> is Group-like associative HGrStr-Family of {1,2,3}
reconsider A = <*G1,G2,G3*> as HGrStr-Family of {1,2,3} ;
A is Group-like

proof

let x be Element of {1,2,3}; :: according to GROUP_7:def 6 :: thesis: A . x is Group-like
( x = 1 or x = 2 or x = 3 ) by ENUMSET1:def 1;
hence A . x is Group-like by FINSEQ_1:62; :: thesis: verum

end;

hence <*G1,G2,G3*> is Group-like associative HGrStr-Family of {1,2,3} ; :: thesis: verum