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;

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;

then A15: f1 * x = 1_ (product F) by A8, A9;

then x * f1 = 1_ (product F) by A8, A16;

hence s = x " by A15, GROUP_1:def 5; :: thesis: verum

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

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

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

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

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

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

then x * f1 = 1_ (product F) by A8, A16;

hence s = x " by A15, GROUP_1:def 5; :: thesis: verum