let I be set ; :: thesis: for g being Function
for s being ManySortedSet of I
for F being Group-like associative multMagma-Family of I
for x being Element of (product F) st x = g & ( for i being set st i in I holds
ex G being Group ex y being Element of G st
( G = F . i & s . i = y " & y = g . i ) ) holds
s = x "
let g be Function; :: thesis: for s being ManySortedSet of I
for F being Group-like associative multMagma-Family of I
for x being Element of (product F) st x = g & ( for i being set st i in I holds
ex G being Group ex y being Element of G st
( G = F . i & s . i = y " & y = g . i ) ) holds
s = x "
let s be ManySortedSet of I; :: thesis: for F being Group-like associative multMagma-Family of I
for x being Element of (product F) st x = g & ( for i being set st i in I holds
ex G being Group ex y being Element of G st
( G = F . i & s . i = y " & y = g . i ) ) holds
s = x "
let F be Group-like associative multMagma-Family of I; :: thesis: for x being Element of (product F) st x = g & ( for i being set st i in I holds
ex G being Group ex y being Element of G st
( G = F . i & s . i = y " & y = g . i ) ) holds
s = x "
let x be Element of (product F); :: thesis: ( x = g & ( for i being set st i in I holds
ex G being Group ex y being Element of G st
( G = F . i & s . i = y " & y = g . i ) ) implies s = x " )
assume that
A1: x = g and
A2: for i being set st i in I holds
ex G being Group ex y being Element of G st
( G = F . i & s . i = y " & y = g . i ) ; :: thesis: s = x "
set GP = product F;
A3: dom (Carrier F) = I by PARTFUN1:def 2;
A4: 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 A5: i in dom s ; :: thesis: s . i in (Carrier F) . i
then A6: ex R being 1-sorted st
( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def 15;
ex G being Group ex y being Element of G st
( G = F . i & s . i = y " & y = g . i ) by A2, A5;
hence s . i in (Carrier F) . i by A6; :: thesis: verum

end;

then A7: s in product (Carrier F) by A3, A4, CARD_3:9;
then reconsider f1 = s as Element of (product F) by Def2;
reconsider II = 1_ (product F), xf = x * f1, fx = f1 * x, x1 = x as Element of product (Carrier F) by Def2;
A8: dom II = I by A3, CARD_3:9;

A9: now :: thesis: for i being object st i in I holds
fx . i = II . i

let i be object ; :: thesis: ( i in I implies fx . i = II . i )
assume A10: i in I ; :: thesis: fx . i = II . i
then consider G being Group, y being Element of G such that
A11: G = F . i and
A12: s . i = y " and
A13: y = g . i by A2;
A14: ex Fi being non empty multMagma ex m being Function st
( Fi = F . i & m = the multF of (product F) . (s,x) & m . i = the multF of Fi . ((s . i),(x1 . i)) ) by A7, A10, Def2;
(y ") * y = 1_ G by GROUP_1:def 5;
hence fx . i = II . i by A1, A10, A14, A11, A12, A13, Th6; :: thesis: verum

end;

dom fx = I by A3, CARD_3:9;
then A15: f1 * x = 1_ (product F) by A8, A9;

A16: now :: thesis: for i being object st i in I holds
xf . i = II . i

let i be object ; :: thesis: ( i in I implies xf . i = II . i )
assume A17: i in I ; :: thesis: xf . i = II . i
then consider G being Group, y being Element of G such that
A18: G = F . i and
A19: s . i = y " and
A20: y = g . i by A2;
A21: ex Fi being non empty multMagma ex m being Function st
( Fi = F . i & m = the multF of (product F) . (x,s) & m . i = the multF of Fi . ((x1 . i),(s . i)) ) by A7, A17, Def2;
y * (y ") = 1_ G by GROUP_1:def 5;
hence xf . i = II . i by A1, A17, A21, A18, A19, A20, Th6; :: thesis: verum

end;

dom xf = I by A3, CARD_3:9;
then x * f1 = 1_ (product F) by A8, A16;
hence s = x " by A15, GROUP_1:def 5; :: thesis: verum