let G1, G2, G3 be non empty Group-like multMagma ; 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 )
proof
let i be
set ;
( 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}
;
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;
suppose A2:
i = 1
;
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
;
( 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;
verum end; suppose A3:
i = 2
;
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
;
( 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;
verum end; suppose A4:
i = 3
;
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
;
( 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;
verum end; end;
end;
hence
1_ (product <*G1,G2,G3*>) = <*(1_ G1),(1_ G2),(1_ G3)*>
by Th5; verum