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 J,D
for X being Element of Fin I st F is having_a_unity & F is commutative & F is associative holds
for y being Element of J st ( for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ) holds
F $$ ([:X,{.y.}:],f) = F $$ ({.y.},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 J,D
for X being Element of Fin I st F is having_a_unity & F is commutative & F is associative holds
for y being Element of J st ( for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ) holds
F $$ ([:X,{.y.}:],f) = F $$ ({.y.},g)
let F be BinOp of D; :: thesis: for f being Function of [:I,J:],D
for g being Function of J,D
for X being Element of Fin I st F is having_a_unity & F is commutative & F is associative holds
for y being Element of J st ( for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ) holds
F $$ ([:X,{.y.}:],f) = F $$ ({.y.},g)
let f be Function of [:I,J:],D; :: thesis: for g being Function of J,D
for X being Element of Fin I st F is having_a_unity & F is commutative & F is associative holds
for y being Element of J st ( for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ) holds
F $$ ([:X,{.y.}:],f) = F $$ ({.y.},g)
let g be Function of J,D; :: thesis: for X being Element of Fin I st F is having_a_unity & F is commutative & F is associative holds
for y being Element of J st ( for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ) holds
F $$ ([:X,{.y.}:],f) = F $$ ({.y.},g)
let X be Element of Fin I; :: thesis: ( F is having_a_unity & F is commutative & F is associative implies for y being Element of J st ( for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ) holds
F $$ ([:X,{.y.}:],f) = F $$ ({.y.},g) )
assume that
A1: F is having_a_unity and
A2: ( F is commutative & F is associative ) ; :: thesis: for y being Element of J st ( for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ) holds
F $$ ([:X,{.y.}:],f) = F $$ ({.y.},g)

now :: thesis: for y being Element of J st ( for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ) holds
F $$ ([:X,{.y.}:],f) = F $$ ({.y.},g)

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

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

let x be object ; :: thesis: ( x in rng h implies x in dom f )
assume x in rng h ; :: thesis: x in dom f
then consider z being object such that
A7: z in dom h and
A8: x = h . z by FUNCT_1:def 3;
x = [z,y] by A4, A7, A8;
hence x 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) = I & rng h c= [:I,J:] ) by A4, FUNCT_2:def 1, RELAT_1:27; :: thesis: verum

end;

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

proof

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

end;

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

proof

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

proof

assume A12: x in [:X,{y}:] ; :: thesis: x in h .: X
then consider x1, y1 being object such that
A13: x = [x1,y1] by RELAT_1:def 1;
A14: y1 in {y} by A12, A13, ZFMISC_1:87;
A15: ( X c= I & x1 in X ) by A12, A13, FINSUB_1:def 5, ZFMISC_1:87;
then h . x1 = [x1,y] by A4
.= x by A13, A14, TARSKI:def 1 ;
hence x in h .: X by A4, A15, FUNCT_1:def 6; :: thesis: verum

end;

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

end;

then A19: h .: X = [: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
[x1,y] = h . x2 by A4, A20, A22
.= [x2,y] 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 I,[:I,J:] by A4, A5, FUNCT_2:2;
thus F $$ ([:X,{.y.}:],f) = F $$ (X,(f * h)) by A1, A2, A23, A19, SETWOP_2:6
.= F $$ (X,((curry' f) . y)) by A5, A9, FUNCT_1:2
.= g . y by A3
.= F $$ ({.y.},g) by A2, SETWISEO:17 ; :: thesis: verum

end;

hence for y being Element of J st ( for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ) holds
F $$ ([:X,{.y.}:],f) = F $$ ({.y.},g) ; :: thesis: verum