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

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₁( set ) -> set = [$1,y];
consider h being Function such that
A4: ( dom h = I & ( for x being set 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 set st x in I holds
g . x = f . x,y ) ) by FUNCT_5:39;
hence dom ((curry' f) . y) = I ; :: thesis: ( dom (f * h) = I & rng h c= [:I,J:] )

now

let x be set ; :: thesis: ( x in rng h implies x in dom f )
assume x in rng h ; :: thesis: x in dom f
then consider z being set such that
A7: z in dom h and
A8: x = h . z by FUNCT_1:def 5;
x = [z,y] by A4, A7, A8;
hence x in dom f by A4, A6, A7, ZFMISC_1:106; :: 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:46; :: thesis: verum

end;

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

proof

let x be set ; :: 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 set st x in I holds
g . x = f . x,y ) ) by FUNCT_5:39;
assume A11: x in I ; :: thesis: ((curry' f) . y) . x = (f * h) . x
hence (f * h) . x = f . (h . x) by A5, FUNCT_1:22
.= f . x,y by A4, A11
.= ((curry' f) . y) . x by A11, A10 ;
:: thesis: verum

end;

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

proof

let x be set ; :: 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 set such that
A13: x = [x1,y1] by RELAT_1:def 1;
A14: y1 in {y} by A12, A13, ZFMISC_1:106;
A15: ( X c= I & x1 in X ) by A12, A13, FINSUB_1:def 5, ZFMISC_1:106;
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 12; :: thesis: verum

end;

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

end;

then A19: h .: X = [:X,{y}:] by TARSKI:2;

now

let x1, x2 be set ; :: 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 ZFMISC_1:33; :: thesis: verum

end;

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