let G1, G2 be non empty Group-like multMagma ; :: thesis: 1_ (product <*G1,G2*>) = <*(1_ G1),(1_ G2)*>
set s = <*(1_ G1),(1_ G2)*>;
set f = <*G1,G2*>;
<*(1_ G1),(1_ G2)*> is ManySortedSet of

proof

dom <*(1_ G1),(1_ G2)*> = {1,2} by FINSEQ_1:4, FINSEQ_3:29;
hence <*(1_ G1),(1_ G2)*> is ManySortedSet of by PARTFUN1:def 4, RELAT_1:def 18; :: thesis: verum

end;

then reconsider s = <*(1_ G1),(1_ G2)*> as ManySortedSet of ;
for i being set st i in {1,2} holds
ex G being non empty Group-like multMagma st
( G = <*G1,G2*> . i & s . i = 1_ G )

proof

let i be set ; :: thesis: ( i in {1,2} implies ex G being non empty Group-like multMagma st
( G = <*G1,G2*> . i & s . i = 1_ G ) )
assume A1: i in {1,2} ; :: thesis: ex G being non empty Group-like multMagma st
( G = <*G1,G2*> . i & s . i = 1_ G )

per cases ( i = 1 or i = 2 ) by A1, TARSKI:def 2;

suppose A2: i = 1 ; :: thesis: ex G being non empty Group-like multMagma st
( G = <*G1,G2*> . i & s . i = 1_ G )

then reconsider G = <*G1,G2*> . i as non empty Group-like multMagma by FINSEQ_1:61;
take G ; :: thesis: ( G = <*G1,G2*> . i & s . i = 1_ G )
<*G1,G2*> . i = G1 by A2, FINSEQ_1:61;
hence ( G = <*G1,G2*> . i & s . i = 1_ G ) by A2, FINSEQ_1:61; :: thesis: verum

end;

suppose A3: i = 2 ; :: thesis: ex G being non empty Group-like multMagma st
( G = <*G1,G2*> . i & s . i = 1_ G )

then reconsider G = <*G1,G2*> . i as non empty Group-like multMagma by FINSEQ_1:61;
take G ; :: thesis: ( G = <*G1,G2*> . i & s . i = 1_ G )
<*G1,G2*> . i = G2 by A3, FINSEQ_1:61;
hence ( G = <*G1,G2*> . i & s . i = 1_ G ) by A3, FINSEQ_1:61; :: thesis: verum

end;

end;

end;

hence 1_ (product <*G1,G2*>) = <*(1_ G1),(1_ G2)*> by Th8; :: thesis: verum