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 FINSEQ_1:89, FINSEQ_3:1;

then reconsider s = <*(1_ G1),(1_ G2),(1_ G3)*> as ManySortedSet of {1,2,3} by PARTFUN1:def 2, RELAT_1:def 18;

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 )

set s = <*(1_ G1),(1_ G2),(1_ G3)*>;

set f = <*G1,G2,G3*>;

dom <*(1_ G1),(1_ G2),(1_ G3)*> = {1,2,3} by FINSEQ_1:89, FINSEQ_3:1;

then reconsider s = <*(1_ G1),(1_ G2),(1_ G3)*> as ManySortedSet of {1,2,3} by PARTFUN1:def 2, RELAT_1:def 18;

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

hence
1_ (product <*G1,G2,G3*>) = <*(1_ G1),(1_ G2),(1_ G3)*>
by Th5; :: thesis: verum
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 )

end;( 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 A1, ENUMSET1:def 1;

end;

suppose A2:
i = 1
; :: thesis: ex G being non empty Group-like multMagma st

( G = <*G1,G2,G3*> . i & s . i = 1_ G )

( 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 A2, FINSEQ_1:45;

hence ( G = <*G1,G2,G3*> . i & s . i = 1_ G ) by A2, FINSEQ_1:45; :: thesis: verum

end;take G ; :: thesis: ( G = <*G1,G2,G3*> . i & s . i = 1_ G )

<*G1,G2,G3*> . i = G1 by A2, FINSEQ_1:45;

hence ( G = <*G1,G2,G3*> . i & s . i = 1_ G ) by A2, FINSEQ_1:45; :: thesis: verum

suppose A3:
i = 2
; :: thesis: ex G being non empty Group-like multMagma st

( G = <*G1,G2,G3*> . i & s . i = 1_ G )

( 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 A3, FINSEQ_1:45;

hence ( G = <*G1,G2,G3*> . i & s . i = 1_ G ) by A3, FINSEQ_1:45; :: thesis: verum

end;take G ; :: thesis: ( G = <*G1,G2,G3*> . i & s . i = 1_ G )

<*G1,G2,G3*> . i = G2 by A3, FINSEQ_1:45;

hence ( G = <*G1,G2,G3*> . i & s . i = 1_ G ) by A3, FINSEQ_1:45; :: thesis: verum

suppose A4:
i = 3
; :: thesis: ex G being non empty Group-like multMagma st

( G = <*G1,G2,G3*> . i & s . i = 1_ G )

( 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 A4, FINSEQ_1:45;

hence ( G = <*G1,G2,G3*> . i & s . i = 1_ G ) by A4, FINSEQ_1:45; :: thesis: verum

end;take G ; :: thesis: ( G = <*G1,G2,G3*> . i & s . i = 1_ G )

<*G1,G2,G3*> . i = G3 by A4, FINSEQ_1:45;

hence ( G = <*G1,G2,G3*> . i & s . i = 1_ G ) by A4, FINSEQ_1:45; :: thesis: verum