let X, Y be set ; :: thesis: for f being Function st dom f = [:X,Y:] holds
( rng (curry f) c= Funcs Y,(rng f) & rng (curry' f) c= Funcs X,(rng f) )
let f be Function; :: thesis: ( dom f = [:X,Y:] implies ( rng (curry f) c= Funcs Y,(rng f) & rng (curry' f) c= Funcs X,(rng f) ) )
assume A1: dom f = [:X,Y:] ; :: thesis: ( rng (curry f) c= Funcs Y,(rng f) & rng (curry' f) c= Funcs X,(rng f) )

A2: now

assume dom f = {} ; :: thesis: ( rng (curry f) c= Funcs Y,(rng f) & rng (curry' f) c= Funcs X,(rng f) )
then A3: ( {} = dom (curry f) & curry' f = curry (~ f) & ( X = {} or Y = {} ) ) by A1, Def3, Th10;
then ( dom (~ f) = [:Y,X:] & [:Y,X:] = {} & dom (curry (~ f)) = proj1 (dom (~ f)) ) by A1, Def3, FUNCT_4:47, ZFMISC_1:113;
then ( rng (curry f) = {} & rng (curry' f) = {} ) by A3, Th10, RELAT_1:65;
hence ( rng (curry f) c= Funcs Y,(rng f) & rng (curry' f) c= Funcs X,(rng f) ) by XBOOLE_1:2; :: thesis: verum

end;

now

assume A4: [:X,Y:] <> {} ; :: thesis: ( rng (curry f) c= Funcs Y,(rng f) & rng (curry' f) c= Funcs X,(rng f) )
then A5: ( dom (curry f) = X & dom (curry' f) = Y ) by A1, Th31;
thus rng (curry f) c= Funcs Y,(rng f) :: thesis: rng (curry' f) c= Funcs X,(rng f)

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng (curry f) or z in Funcs Y,(rng f) )
assume z in rng (curry f) ; :: thesis: z in Funcs Y,(rng f)
then consider x being set such that
A6: ( x in dom (curry f) & z = (curry f) . x ) by FUNCT_1:def 5;
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 ) ) by A1, A4, A5, A6, Th36;
hence z in Funcs Y,(rng f) by A6, FUNCT_2:def 2; :: thesis: verum

end;

thus rng (curry' f) c= Funcs X,(rng f) :: thesis: verum

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng (curry' f) or z in Funcs X,(rng f) )
assume z in rng (curry' f) ; :: thesis: z in Funcs X,(rng f)
then consider y being set such that
A7: ( y in dom (curry' f) & z = (curry' f) . y ) by FUNCT_1:def 5;
ex g being Function st
( (curry' f) . y = g & dom g = X & rng g c= rng f & ( for x being set st x in X holds
g . x = f . x,y ) ) by A1, A4, A5, A7, Th39;
hence z in Funcs X,(rng f) by A7, FUNCT_2:def 2; :: thesis: verum

end;

end;

hence ( rng (curry f) c= Funcs Y,(rng f) & rng (curry' f) c= Funcs X,(rng f) ) by A1, A2; :: thesis: verum