let X, Y be set ; :: thesis: 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 ; :: thesis: 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; :: thesis: ( [: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 ; :: thesis: 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 ; :: thesis: ( (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
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng g or z in rng f )
assume z in rng g ; :: thesis: z in rng f
then consider y being object such that
A9: ( y in dom g & z = g . y ) by FUNCT_1:def 3;
( [x,y] in dom f & z = f . (x,y) ) by A2, A3, A6, A8, A4, A7, A9, ZFMISC_1:87;
hence z in rng f by FUNCT_1:def 3; :: thesis: verum
end;
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; :: thesis: verum