let X, Y be set ; for x being object
for f being Function st [:X,Y:] <> {} & dom f = [:X,Y:] & x in X holds
ex g being Function st
( (curry f) . x = g & dom g = Y & rng g c= rng f & ( for y being object st y in Y holds
g . y = f . (x,y) ) )
let x be object ; for f being Function st [:X,Y:] <> {} & dom f = [:X,Y:] & x in X holds
ex g being Function st
( (curry f) . x = g & dom g = Y & rng g c= rng f & ( for y being object st y in Y holds
g . y = f . (x,y) ) )
let f be Function; ( [:X,Y:] <> {} & dom f = [:X,Y:] & x in X implies ex g being Function st
( (curry f) . x = g & dom g = Y & rng g c= rng f & ( for y being object st y in Y holds
g . y = f . (x,y) ) ) )
assume that
A1:
[:X,Y:] <> {}
and
A2:
dom f = [:X,Y:]
and
A3:
x in X
; ex g being Function st
( (curry f) . x = g & dom g = Y & rng g c= rng f & ( for y being object st y in Y holds
g . y = f . (x,y) ) )
{x} c= X
by A3, ZFMISC_1:31;
then A4:
[:{x},Y:] /\ (dom f) = [:{x},Y:]
by A2, ZFMISC_1:101;
x in proj1 (dom f)
by A1, A2, A3, Th3;
then consider g being Function such that
A5:
(curry f) . x = g
and
A6:
( dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being object st y in dom g holds
g . y = f . (x,y) ) )
by Def1;
take
g
; ( (curry f) . x = g & dom g = Y & rng g c= rng f & ( for y being object st y in Y holds
g . y = f . (x,y) ) )
A7:
proj2 [:{x},Y:] = Y
by Th3;
A8:
proj2 (dom f) = Y
by A2, A3, Th3;
rng g c= rng f
hence
( (curry f) . x = g & dom g = Y & rng g c= rng f & ( for y being object st y in Y holds
g . y = f . (x,y) ) )
by A5, A6, A8, A4, A7; verum