let D be non empty set ; :: thesis: for I, J being non empty set
for F being BinOp of D
for f being Function of [:I,J:],D
for g being Function of I,D
for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp holds
for x being Element of I st ( for i being Element of I holds g . i = F $$ Y,((curry f) . i) ) holds
F $$ [:{.x.},Y:],f = F $$ {.x.},g
let I, J be non empty set ; :: thesis: for F being BinOp of D
for f being Function of [:I,J:],D
for g being Function of I,D
for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp holds
for x being Element of I st ( for i being Element of I holds g . i = F $$ Y,((curry f) . i) ) holds
F $$ [:{.x.},Y:],f = F $$ {.x.},g
let F be BinOp of D; :: thesis: for f being Function of [:I,J:],D
for g being Function of I,D
for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp holds
for x being Element of I st ( for i being Element of I holds g . i = F $$ Y,((curry f) . i) ) holds
F $$ [:{.x.},Y:],f = F $$ {.x.},g
let f be Function of [:I,J:],D; :: thesis: for g being Function of I,D
for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp holds
for x being Element of I st ( for i being Element of I holds g . i = F $$ Y,((curry f) . i) ) holds
F $$ [:{.x.},Y:],f = F $$ {.x.},g
let g be Function of I,D; :: thesis: for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp holds
for x being Element of I st ( for i being Element of I holds g . i = F $$ Y,((curry f) . i) ) holds
F $$ [:{.x.},Y:],f = F $$ {.x.},g
let Y be Element of Fin J; :: thesis: ( F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp implies for x being Element of I st ( for i being Element of I holds g . i = F $$ Y,((curry f) . i) ) holds
F $$ [:{.x.},Y:],f = F $$ {.x.},g )
assume A1: ( F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp ) ; :: thesis: for x being Element of I st ( for i being Element of I holds g . i = F $$ Y,((curry f) . i) ) holds
F $$ [:{.x.},Y:],f = F $$ {.x.},g

now

let x be Element of I; :: thesis: ( ( for i being Element of I holds g . i = F $$ Y,((curry f) . i) ) implies F $$ [:{.x.},Y:],f = F $$ {.x.},g )
assume A2: for i being Element of I holds g . i = F $$ Y,((curry f) . i) ; :: thesis: F $$ [:{.x.},Y:],f = F $$ {.x.},g
deffunc H₁( set ) -> set = [x,$1];
consider h being Function such that
A3: ( dom h = J & ( for y being set st y in J holds
h . y = H₁(y) ) ) from FUNCT_1:sch 3();
A4: h is one-to-one

proof

now

let x1, x2 be set ; :: thesis: ( x1 in dom h & x2 in dom h & h . x1 = h . x2 implies x1 = x2 )
assume A5: ( x1 in dom h & x2 in dom h & h . x1 = h . x2 ) ; :: thesis: x1 = x2
then [x,x1] = h . x2 by A3
.= [x,x2] by A3, A5 ;
hence x1 = x2 by ZFMISC_1:33; :: thesis: verum

end;

hence h is one-to-one by FUNCT_1:def 8; :: thesis: verum

end;

A6: h .: Y = [:{x},Y:]

proof

for y being set holds
( y in [:{x},Y:] iff y in h .: Y )

proof

let y be set ; :: thesis: ( y in [:{x},Y:] iff y in h .: Y )
thus ( y in [:{x},Y:] implies y in h .: Y ) :: thesis: ( y in h .: Y implies y in [:{x},Y:] )

proof

assume A7: y in [:{x},Y:] ; :: thesis: y in h .: Y
then consider y1, x1 being set such that
A8: y = [y1,x1] by RELAT_1:def 1;
A9: Y c= J by FINSUB_1:def 5;
A10: ( y1 in {x} & x1 in Y ) by A7, A8, ZFMISC_1:106;
then h . x1 = [x,x1] by A3, A9
.= y by A8, A10, TARSKI:def 1 ;
hence y in h .: Y by A3, A9, A10, FUNCT_1:def 12; :: thesis: verum

end;

assume y in h .: Y ; :: thesis: y in [:{x},Y:]
then consider z being set such that
A11: ( z in dom h & z in Y & y = h . z ) by FUNCT_1:def 12;
y = [x,z] by A3, A11;
hence y in [:{x},Y:] by A11, ZFMISC_1:128; :: thesis: verum

end;

hence h .: Y = [:{x},Y:] by TARSKI:2; :: thesis: verum

end;

A12: ( dom ((curry f) . x) = J & dom (f * h) = J & rng h c= [:I,J:] )

proof

A13: dom f = [:I,J:] by FUNCT_2:def 1;
then consider g being Function such that
A14: ( g = (curry f) . x & dom g = J & rng g c= rng f & ( for y being set st y in J holds
g . y = f . x,y ) ) by FUNCT_5:36;
thus dom ((curry f) . x) = J by A14; :: thesis: ( dom (f * h) = J & rng h c= [:I,J:] )

now

let y be set ; :: thesis: ( y in rng h implies y in dom f )
assume y in rng h ; :: thesis: y in dom f
then consider z being set such that
A15: ( z in dom h & y = h . z ) by FUNCT_1:def 5;
y = [x,z] by A3, A15;
hence y in dom f by A3, A13, A15, ZFMISC_1:106; :: thesis: verum

end;

then rng h c= dom f by TARSKI:def 3;
hence ( dom (f * h) = J & rng h c= [:I,J:] ) by A3, FUNCT_2:def 1, RELAT_1:46; :: thesis: verum

end;

A16: for y being set st y in J holds
((curry f) . x) . y = (f * h) . y

proof

let y be set ; :: thesis: ( y in J implies ((curry f) . x) . y = (f * h) . y )
assume A17: y in J ; :: thesis: ((curry f) . x) . y = (f * h) . y
dom f = [:I,J:] by FUNCT_2:def 1;
then consider g being Function such that
A18: ( g = (curry f) . x & dom g = J & rng g c= rng f & ( for y being set st y in J holds
g . y = f . x,y ) ) by FUNCT_5:36;
thus (f * h) . y = f . (h . y) by A12, A17, FUNCT_1:22
.= f . x,y by A3, A17
.= ((curry f) . x) . y by A17, A18 ; :: thesis: verum

end;

reconsider h = h as Function of J,[:I,J:] by A3, A12, FUNCT_2:4;
thus F $$ [:{.x.},Y:],f = F $$ Y,(f * h) by A1, A4, A6, SETWOP_2:8
.= F $$ Y,((curry f) . x) by A12, A16, FUNCT_1:9
.= g . x by A2
.= F $$ {.x.},g by A1, SETWISEO:26 ; :: thesis: verum

end;

hence for x being Element of I st ( for i being Element of I holds g . i = F $$ Y,((curry f) . i) ) holds
F $$ [:{.x.},Y:],f = F $$ {.x.},g ; :: thesis: verum