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 () 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 () 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 () 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 () 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 (); :: 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 () = 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 () . i
let i be object ; :: thesis: ( i in dom s implies s . i in () . i )
assume A5: i in dom s ; :: thesis: s . i in () . i
then A6: ex R being 1-sorted st
( R = F . i & () . i = the carrier of R ) by PRALG_1:def 13;
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 () . i by A6; :: thesis: verum
end;
then A7: s in product () by ;
then reconsider f1 = s as Element of () by Def2;
reconsider II = 1_ (), xf = x * f1, fx = f1 * x, x1 = x as Element of product () by Def2;
A8: dom II = I by ;
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 () . (s,x) & m . i = the multF of Fi . ((s . i),(x1 . i)) ) by ;
(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 ;
then A15: f1 * x = 1_ () 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 () . (x,s) & m . i = the multF of Fi . ((x1 . i),(s . i)) ) by ;
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 ;
then x * f1 = 1_ () by ;
hence s = x " by ; :: thesis: verum