let X, Y, x be set ; :: 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 set 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 set st y in Y holds
g . y = f . x,y ) ) )
assume A1: ( [:X,Y:] <> {} & dom f = [:X,Y:] & x in X ) ; :: thesis: ex g being Function st
( (curry f) . x = g & dom g = Y & rng g c= rng f & ( for y being set st y in Y holds
g . y = f . x,y ) )
then x in proj1 (dom f) by Th11;
then consider g being Function such that
A2: ( (curry f) . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g holds
g . y = f . x,y ) ) by Def3;
take g ; :: thesis: ( (curry f) . x = g & dom g = Y & rng g c= rng f & ( for y being set st y in Y holds
g . y = f . x,y ) )
( X <> {} & {x} c= X & Y c= Y ) by A1, ZFMISC_1:37;
then A3: ( proj2 (dom f) = Y & (dom f) /\ [:{x},Y:] = [:{x},Y:] /\ (dom f) & [:{x},Y:] /\ (dom f) = [:{x},Y:] & proj2 [:{x},Y:] = Y ) by A1, Th11, ZFMISC_1:124;
rng g c= rng f

proof

let z be set ; :: 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 set such that
A4: ( y in dom g & z = g . y ) by FUNCT_1:def 5;
( [x,y] in dom f & z = f . x,y ) by A1, A2, A3, A4, ZFMISC_1:106;
hence z in rng f by FUNCT_1:def 5; :: thesis: verum

end;

hence ( (curry f) . x = g & dom g = Y & rng g c= rng f & ( for y being set st y in Y holds
g . y = f . x,y ) ) by A2, A3; :: thesis: verum