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 & F is having_an_inverseOp 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 & F is having_an_inverseOp 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 & F is having_an_inverseOp 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 & F is having_an_inverseOp 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 & F is having_an_inverseOp 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 & F is having_an_inverseOp 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 A1: ( F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp ) ; :: 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 A2: 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
A3: ( dom h = I & ( for x being set st x in I holds
h . x = H₁(x) ) ) 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 [x1,y] = h . x2 by A3
.= [x2,y] 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 .: X = [:X,{y}:]

proof

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 A7: x in [:X,{y}:] ; :: thesis: x in h .: X
then consider x1, y1 being set such that
A8: x = [x1,y1] by RELAT_1:def 1;
A9: X c= I by FINSUB_1:def 5;
A10: ( x1 in X & y1 in {y} ) by A7, A8, ZFMISC_1:106;
then h . x1 = [x1,y] by A3, A9
.= x by A8, A10, TARSKI:def 1 ;
hence x in h .: X by A3, A9, A10, FUNCT_1:def 12; :: thesis: verum

end;

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

end;

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

end;

A12: ( dom ((curry' f) . y) = I & dom (f * h) = I & 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) . 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;
thus dom ((curry' f) . y) = I by A14; :: 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
A15: ( z in dom h & x = h . z ) by FUNCT_1:def 5;
x = [z,y] by A3, A15;
hence x 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) = I & rng h c= [:I,J:] ) by A3, FUNCT_2:def 1, RELAT_1:46; :: thesis: verum

end;

A16: 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 )
assume A17: x in I ; :: thesis: ((curry' f) . y) . x = (f * h) . x
dom f = [:I,J:] by FUNCT_2:def 1;
then consider g being Function such that
A18: ( 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;
thus (f * h) . x = f . (h . x) by A12, A17, FUNCT_1:22
.= f . x,y by A3, A17
.= ((curry' f) . y) . x by A17, A18 ; :: thesis: verum

end;

reconsider h = h as Function of I,[:I,J:] by A3, A12, FUNCT_2:4;
thus F $$ [:X,{.y.}:],f = F $$ X,(f * h) by A1, A4, A6, SETWOP_2:8
.= F $$ X,((curry' f) . y) by A12, A16, FUNCT_1:9
.= g . y by A2
.= F $$ {.y.},g by A1, 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