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 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 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 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 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 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 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 that
A1: F is having_a_unity and
A2: ( F is commutative & F is associative ) ; :: 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 :: 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)

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 A3: for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ; :: thesis: F $$ ([:{.x.},Y:],f) = F $$ ({.x.},g)
deffunc H₁( object ) -> object = [x,$1];
consider h being Function such that
A4: ( dom h = J & ( for y being object st y in J holds
h . y = H₁(y) ) ) from FUNCT_1:sch 3();
A5: ( dom ((curry f) . x) = J & dom (f * h) = J & rng h c= [:I,J:] )

proof

A6: dom f = [:I,J:] by FUNCT_2:def 1;
then ex g being Function st
( g = (curry f) . x & dom g = J & rng g c= rng f & ( for y being object st y in J holds
g . y = f . (x,y) ) ) by FUNCT_5:29;
hence dom ((curry f) . x) = J ; :: thesis: ( dom (f * h) = J & rng h c= [:I,J:] )

now :: thesis: for y being object st y in rng h holds
y in dom f

let y be object ; :: thesis: ( y in rng h implies y in dom f )
assume y in rng h ; :: thesis: y in dom f
then consider z being object such that
A7: z in dom h and
A8: y = h . z by FUNCT_1:def 3;
y = [x,z] by A4, A7, A8;
hence y in dom f by A4, A6, A7, ZFMISC_1:87; :: thesis: verum

end;

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

end;

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

proof

let y be object ; :: thesis: ( y in J implies ((curry f) . x) . y = (f * h) . y )
dom f = [:I,J:] by FUNCT_2:def 1;
then A10: ex g being Function st
( g = (curry f) . x & dom g = J & rng g c= rng f & ( for y being object st y in J holds
g . y = f . (x,y) ) ) by FUNCT_5:29;
assume A11: y in J ; :: thesis: ((curry f) . x) . y = (f * h) . y
hence (f * h) . y = f . (h . y) by A5, FUNCT_1:12
.= f . (x,y) by A4, A11
.= ((curry f) . x) . y by A11, A10 ;
:: thesis: verum

end;

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

proof

let y be object ; :: 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 A12: y in [:{x},Y:] ; :: thesis: y in h .: Y
then consider y1, x1 being object such that
A13: y = [y1,x1] by RELAT_1:def 1;
A14: y1 in {x} by A12, A13, ZFMISC_1:87;
A15: ( Y c= J & x1 in Y ) by A12, A13, FINSUB_1:def 5, ZFMISC_1:87;
then h . x1 = [x,x1] by A4
.= y by A13, A14, TARSKI:def 1 ;
hence y in h .: Y by A4, A15, FUNCT_1:def 6; :: thesis: verum

end;

assume y in h .: Y ; :: thesis: y in [:{x},Y:]
then consider z being object such that
A16: z in dom h and
A17: z in Y and
A18: y = h . z by FUNCT_1:def 6;
y = [x,z] by A4, A16, A18;
hence y in [:{x},Y:] by A17, ZFMISC_1:105; :: thesis: verum

end;

then A19: h .: Y = [:{x},Y:] by TARSKI:2;

now :: thesis: for x1, x2 being object st x1 in dom h & x2 in dom h & h . x1 = h . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom h & x2 in dom h & h . x1 = h . x2 implies x1 = x2 )
assume that
A20: x1 in dom h and
A21: x2 in dom h and
A22: h . x1 = h . x2 ; :: thesis: x1 = x2
[x,x1] = h . x2 by A4, A20, A22
.= [x,x2] by A4, A21 ;
hence x1 = x2 by XTUPLE_0:1; :: thesis: verum

end;

then A23: h is one-to-one by FUNCT_1:def 4;
reconsider h = h as Function of J,[:I,J:] by A4, A5, FUNCT_2:2;
thus F $$ ([:{.x.},Y:],f) = F $$ (Y,(f * h)) by A1, A2, A23, A19, SETWOP_2:6
.= F $$ (Y,((curry f) . x)) by A5, A9, FUNCT_1:2
.= g . x by A3
.= F $$ ({.x.},g) by A2, SETWISEO:17 ; :: 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