let G1 be non empty multMagma ; :: thesis: <*G1*> is multMagma-Family of
A1: dom <*G1*> = {1} by FINSEQ_1:4, FINSEQ_1:def 8;
then reconsider A = <*G1*> as ManySortedSet of by PARTFUN1:def 4, RELAT_1:def 18;
A is multMagma-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 by A1, A2, TARSKI:def 1;
hence y is non empty multMagma by A2, FINSEQ_1:def 8; :: thesis: verum

end;

hence <*G1*> is multMagma-Family of ; :: thesis: verum