let I be set ; :: thesis: for s being ManySortedSet of I

for F being Group-like multMagma-Family of I st ( for i being set st i in I holds

ex G being non empty Group-like multMagma st

( G = F . i & s . i = 1_ G ) ) holds

s = 1_ (product F)

let s be ManySortedSet of I; :: thesis: for F being Group-like multMagma-Family of I st ( for i being set st i in I holds

ex G being non empty Group-like multMagma st

( G = F . i & s . i = 1_ G ) ) holds

s = 1_ (product F)

let F be Group-like multMagma-Family of I; :: thesis: ( ( for i being set st i in I holds

ex G being non empty Group-like multMagma st

( G = F . i & s . i = 1_ G ) ) implies s = 1_ (product F) )

assume A1: for i being set st i in I holds

ex G being non empty Group-like multMagma st

( G = F . i & s . i = 1_ G ) ; :: thesis: s = 1_ (product F)

set GP = product F;

A2: dom (Carrier F) = I by PARTFUN1:def 2;

A3: dom s = I by PARTFUN1:def 2;

then reconsider e = s as Element of (product F) by Def2;

for F being Group-like multMagma-Family of I st ( for i being set st i in I holds

ex G being non empty Group-like multMagma st

( G = F . i & s . i = 1_ G ) ) holds

s = 1_ (product F)

let s be ManySortedSet of I; :: thesis: for F being Group-like multMagma-Family of I st ( for i being set st i in I holds

ex G being non empty Group-like multMagma st

( G = F . i & s . i = 1_ G ) ) holds

s = 1_ (product F)

let F be Group-like multMagma-Family of I; :: thesis: ( ( for i being set st i in I holds

ex G being non empty Group-like multMagma st

( G = F . i & s . i = 1_ G ) ) implies s = 1_ (product F) )

assume A1: for i being set st i in I holds

ex G being non empty Group-like multMagma st

( G = F . i & s . i = 1_ G ) ; :: thesis: s = 1_ (product F)

set GP = product F;

A2: dom (Carrier F) = I by PARTFUN1:def 2;

A3: dom s = I by PARTFUN1:def 2;

now :: thesis: for i being object st i in dom s holds

s . i in (Carrier F) . i

then A6:
s in product (Carrier F)
by A3, A2, CARD_3:9;s . i in (Carrier F) . i

let i be object ; :: thesis: ( i in dom s implies s . i in (Carrier F) . i )

assume A4: i in dom s ; :: thesis: s . i in (Carrier F) . i

then A5: ex R being 1-sorted st

( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def 13;

ex G being non empty Group-like multMagma st

( G = F . i & s . i = 1_ G ) by A1, A4;

hence s . i in (Carrier F) . i by A5; :: thesis: verum

end;assume A4: i in dom s ; :: thesis: s . i in (Carrier F) . i

then A5: ex R being 1-sorted st

( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def 13;

ex G being non empty Group-like multMagma st

( G = F . i & s . i = 1_ G ) by A1, A4;

hence s . i in (Carrier F) . i by A5; :: thesis: verum

then reconsider e = s as Element of (product F) by Def2;

now :: thesis: for h being Element of (product F) holds

( h * e = h & e * h = h )

hence
s = 1_ (product F)
by GROUP_1:4; :: thesis: verum( h * e = h & e * h = h )

let h be Element of (product F); :: thesis: ( h * e = h & e * h = h )

reconsider h1 = h, he = h * e, eh = e * h as Element of product (Carrier F) by Def2;

A7: dom h1 = I by A2, CARD_3:9;

hence h * e = h by A7, A8; :: thesis: e * h = h

hence e * h = h by A7, A13; :: thesis: verum

end;reconsider h1 = h, he = h * e, eh = e * h as Element of product (Carrier F) by Def2;

A7: dom h1 = I by A2, CARD_3:9;

A8: now :: thesis: for i being object st i in I holds

he . i = h1 . i

dom he = I
by A2, CARD_3:9;he . i = h1 . i

let i be object ; :: thesis: ( i in I implies he . i = h1 . i )

assume A9: i in I ; :: thesis: he . i = h1 . i

then consider G being non empty Group-like multMagma such that

A10: G = F . i and

A11: s . i = 1_ G by A1;

reconsider b = h1 . i, c = s . i as Element of G by A9, A10, A11, Lm1;

A12: ex Fi being non empty multMagma ex m being Function st

( Fi = F . i & m = the multF of (product F) . (h,s) & m . i = the multF of Fi . ((h1 . i),(s . i)) ) by A6, A9, Def2;

b * c = b by A11, GROUP_1:def 4;

hence he . i = h1 . i by A12, A10; :: thesis: verum

end;assume A9: i in I ; :: thesis: he . i = h1 . i

then consider G being non empty Group-like multMagma such that

A10: G = F . i and

A11: s . i = 1_ G by A1;

reconsider b = h1 . i, c = s . i as Element of G by A9, A10, A11, Lm1;

A12: ex Fi being non empty multMagma ex m being Function st

( Fi = F . i & m = the multF of (product F) . (h,s) & m . i = the multF of Fi . ((h1 . i),(s . i)) ) by A6, A9, Def2;

b * c = b by A11, GROUP_1:def 4;

hence he . i = h1 . i by A12, A10; :: thesis: verum

hence h * e = h by A7, A8; :: thesis: e * h = h

A13: now :: thesis: for i being object st i in I holds

eh . i = h1 . i

dom eh = I
by A2, CARD_3:9;eh . i = h1 . i

let i be object ; :: thesis: ( i in I implies eh . i = h1 . i )

assume A14: i in I ; :: thesis: eh . i = h1 . i

then consider G being non empty Group-like multMagma such that

A15: G = F . i and

A16: s . i = 1_ G by A1;

reconsider b = h1 . i, c = s . i as Element of G by A14, A15, A16, Lm1;

A17: ex Fi being non empty multMagma ex m being Function st

( Fi = F . i & m = the multF of (product F) . (s,h) & m . i = the multF of Fi . ((s . i),(h1 . i)) ) by A6, A14, Def2;

c * b = b by A16, GROUP_1:def 4;

hence eh . i = h1 . i by A17, A15; :: thesis: verum

end;assume A14: i in I ; :: thesis: eh . i = h1 . i

then consider G being non empty Group-like multMagma such that

A15: G = F . i and

A16: s . i = 1_ G by A1;

reconsider b = h1 . i, c = s . i as Element of G by A14, A15, A16, Lm1;

A17: ex Fi being non empty multMagma ex m being Function st

( Fi = F . i & m = the multF of (product F) . (s,h) & m . i = the multF of Fi . ((s . i),(h1 . i)) ) by A6, A14, Def2;

c * b = b by A16, GROUP_1:def 4;

hence eh . i = h1 . i by A17, A15; :: thesis: verum

hence e * h = h by A7, A13; :: thesis: verum