let I be set ; :: thesis: for s being ManySortedSet of I
for F being Group-like HGrStr-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 HGrStr-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 HGrStr-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 s = I by PBOOLE:def 3;
A3: dom (Carrier F) = I by PBOOLE:def 3;

now

let i be set ; :: 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 consider G being non empty Group-like multMagma such that
A5: ( G = F . i & s . i = 1_ G ) by A1, A2;
consider R being 1-sorted such that
A6: ( R = F . i & (Carrier F) . i = the carrier of R ) by A2, A4, PRALG_1:def 13;
thus s . i in (Carrier F) . i by A5, A6; :: thesis: verum

end;

then A7: s in product (Carrier F) by A2, A3, CARD_3:18;
then reconsider e = s as Element of (product F) by Def2;

now

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;
A8: ( dom he = I & dom eh = I & dom h1 = I ) by A3, CARD_3:18;

now

let i be set ; :: thesis: ( i in I implies he . i = h1 . i )
assume A9: i in I ; :: thesis: he . i = h1 . i
then consider Fi being non empty multMagma , m being Function such that
A10: ( Fi = F . i & m = the multF of (product F) . h,s & m . i = the multF of Fi . (h1 . i),(s . i) ) by A7, Def2;
consider G being non empty Group-like multMagma such that
A11: ( G = F . i & s . i = 1_ G ) by A1, A9;
reconsider b = h1 . i, c = s . i as Element of G by A9, A11, Lm1;
b * c = b by A11, GROUP_1:def 5;
hence he . i = h1 . i by A10, A11; :: thesis: verum

end;

hence h * e = h by A8, FUNCT_1:9; :: thesis: e * h = h

now

let i be set ; :: thesis: ( i in I implies eh . i = h1 . i )
assume A12: i in I ; :: thesis: eh . i = h1 . i
then consider Fi being non empty multMagma , m being Function such that
A13: ( Fi = F . i & m = the multF of (product F) . s,h & m . i = the multF of Fi . (s . i),(h1 . i) ) by A7, Def2;
consider G being non empty Group-like multMagma such that
A14: ( G = F . i & s . i = 1_ G ) by A1, A12;
reconsider b = h1 . i, c = s . i as Element of G by A12, A14, Lm1;
c * b = b by A14, GROUP_1:def 5;
hence eh . i = h1 . i by A13, A14; :: thesis: verum

end;

hence e * h = h by A8, FUNCT_1:9; :: thesis: verum

end;

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