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;

now :: thesis: for i being object st i in dom s holds
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 15;
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;

then A6: s in product (Carrier F) by A3, A2, CARD_3:9;
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 )

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;

A8: now :: thesis: for i being object st i in I holds
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;

dom he = I by A2, CARD_3:9;
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

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;

dom eh = I by A2, CARD_3:9;
hence e * h = h by A7, A13; :: thesis: verum

end;

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