let G1 be non empty Group-like multMagma ; :: thesis: 1_ (product <*G1*>) = <*(1_ G1)*>

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

set f = <*G1*>;

dom <*(1_ G1)*> = {1} by FINSEQ_1:2, FINSEQ_1:def 8;

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

for i being set st i in {1} holds

ex G being non empty Group-like multMagma st

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

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

set f = <*G1*>;

dom <*(1_ G1)*> = {1} by FINSEQ_1:2, FINSEQ_1:def 8;

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

for i being set st i in {1} holds

ex G being non empty Group-like multMagma st

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

proof

hence
1_ (product <*G1*>) = <*(1_ G1)*>
by Th5; :: thesis: verum
let i be set ; :: thesis: ( i in {1} implies ex G being non empty Group-like multMagma st

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

assume i in {1} ; :: thesis: ex G being non empty Group-like multMagma st

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

then A1: i = 1 by TARSKI:def 1;

then reconsider G = <*G1*> . i as non empty Group-like multMagma by FINSEQ_1:def 8;

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

<*G1*> . i = G1 by A1, FINSEQ_1:def 8;

hence ( G = <*G1*> . i & s . i = 1_ G ) by A1, FINSEQ_1:def 8; :: thesis: verum

end;( G = <*G1*> . i & s . i = 1_ G ) )

assume i in {1} ; :: thesis: ex G being non empty Group-like multMagma st

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

then A1: i = 1 by TARSKI:def 1;

then reconsider G = <*G1*> . i as non empty Group-like multMagma by FINSEQ_1:def 8;

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

<*G1*> . i = G1 by A1, FINSEQ_1:def 8;

hence ( G = <*G1*> . i & s . i = 1_ G ) by A1, FINSEQ_1:def 8; :: thesis: verum