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

dom <*G1,G2*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;

then reconsider A = <*G1,G2*> as ManySortedSet of {1,2} by PARTFUN1:def 2, RELAT_1:def 18;

A is multMagma-yielding

dom <*G1,G2*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;

then reconsider A = <*G1,G2*> as ManySortedSet of {1,2} by PARTFUN1:def 2, RELAT_1:def 18;

A is multMagma-yielding

proof

hence
<*G1,G2*> is multMagma-Family of {1,2}
; :: thesis: verum
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 object such that

A1: x in dom A and

A2: A . x = y by FUNCT_1:def 3;

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

hence y is non empty multMagma by A2, FINSEQ_1:44; :: thesis: verum

end;assume y in rng A ; :: thesis: y is non empty multMagma

then consider x being object such that

A1: x in dom A and

A2: A . x = y by FUNCT_1:def 3;

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

hence y is non empty multMagma by A2, FINSEQ_1:44; :: thesis: verum