let G1, G2, G3 be non empty Group-like multMagma ; :: thesis: 1_ (product <*G1,G2,G3*>) = <*(1_ G1),(1_ G2),(1_ G3)*>
set s = <*(1_ G1),(1_ G2),(1_ G3)*>;
set f = <*G1,G2,G3*>;
dom <*(1_ G1),(1_ G2),(1_ G3)*> = {1,2,3} by ;
then reconsider s = <*(1_ G1),(1_ G2),(1_ G3)*> as ManySortedSet of {1,2,3} by ;
for i being set st i in {1,2,3} holds
ex G being non empty Group-like multMagma st
( G = <*G1,G2,G3*> . i & s . i = 1_ G )
proof
let i be set ; :: thesis: ( i in {1,2,3} implies ex G being non empty Group-like multMagma st
( G = <*G1,G2,G3*> . i & s . i = 1_ G ) )

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

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

then reconsider G = <*G1,G2,G3*> . i as non empty Group-like multMagma by FINSEQ_1:45;
take G ; :: thesis: ( G = <*G1,G2,G3*> . i & s . i = 1_ G )
<*G1,G2,G3*> . i = G1 by ;
hence ( G = <*G1,G2,G3*> . i & s . i = 1_ G ) by ; :: thesis: verum
end;
suppose A3: i = 2 ; :: thesis: ex G being non empty Group-like multMagma st
( G = <*G1,G2,G3*> . i & s . i = 1_ G )

then reconsider G = <*G1,G2,G3*> . i as non empty Group-like multMagma by FINSEQ_1:45;
take G ; :: thesis: ( G = <*G1,G2,G3*> . i & s . i = 1_ G )
<*G1,G2,G3*> . i = G2 by ;
hence ( G = <*G1,G2,G3*> . i & s . i = 1_ G ) by ; :: thesis: verum
end;
suppose A4: i = 3 ; :: thesis: ex G being non empty Group-like multMagma st
( G = <*G1,G2,G3*> . i & s . i = 1_ G )

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