let G1, G2, G3 be non empty multMagma ; :: thesis: <*G1,G2,G3*> is HGrStr-Family of {1,2,3}
A1: dom <*G1,G2,G3*> = {1,2,3} by FINSEQ_3:1, FINSEQ_3:30;
then reconsider A = <*G1,G2,G3*> as ManySortedSet of {1,2,3} by PBOOLE:def 3;
A is HGrStr-yielding

proof

let y be set ; :: according to GROUP_7:def 1 :: thesis: ( y in rng A implies y is non empty multMagma )
assume y in rng A ; :: thesis: y is non empty multMagma
then consider x being set such that
A2: ( x in dom A & A . x = y ) by FUNCT_1:def 5;
( x = 1 or x = 2 or x = 3 ) by A1, A2, ENUMSET1:def 1;
hence y is non empty multMagma by A2, FINSEQ_1:62; :: thesis: verum

end;

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