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_ ()

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_ ()

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_ () )

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_ ()
set GP = product F;
A2: dom () = 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 () . i
let i be object ; :: thesis: ( i in dom s implies s . i in () . i )
assume A4: i in dom s ; :: thesis: s . i in () . i
then A5: ex R being 1-sorted st
( R = F . i & () . 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 () . i by A5; :: thesis: verum
end;
then A6: s in product () by ;
then reconsider e = s as Element of () by Def2;
now :: thesis: for h being Element of () holds
( h * e = h & e * h = h )
let h be Element of (); :: thesis: ( h * e = h & e * h = h )
reconsider h1 = h, he = h * e, eh = e * h as Element of product () by Def2;
A7: dom h1 = I by ;
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 () . (h,s) & m . i = the multF of Fi . ((h1 . i),(s . i)) ) by A6, A9, Def2;
b * c = b by ;
hence he . i = h1 . i by ; :: thesis: verum
end;
dom he = I by ;
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 () . (s,h) & m . i = the multF of Fi . ((s . i),(h1 . i)) ) by ;
c * b = b by ;
hence eh . i = h1 . i by ; :: thesis: verum
end;
dom eh = I by ;
hence e * h = h by ; :: thesis: verum
end;
hence s = 1_ () by GROUP_1:4; :: thesis: verum