let f be Function; :: thesis: ( rng (curry f) c= PFuncs (proj2 (dom f)),(rng f) & rng (curry' f) c= PFuncs (proj1 (dom f)),(rng f) )
thus rng (curry f) c= PFuncs (proj2 (dom f)),(rng f) :: thesis: rng (curry' f) c= PFuncs (proj1 (dom f)),(rng f)

proof

let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in rng (curry f) or t in PFuncs (proj2 (dom f)),(rng f) )
assume t in rng (curry f) ; :: thesis: t in PFuncs (proj2 (dom f)),(rng f)
then consider z being set such that
A1: ( z in dom (curry f) & t = (curry f) . z ) by FUNCT_1:def 5;
dom (curry f) = proj1 (dom f) by Def3;
then consider g being Function such that
A2: ( (curry f) . z = g & dom g = proj2 ((dom f) /\ [:{z},(proj2 (dom f)):]) & ( for y being set st y in dom g holds
g . y = f . z,y ) ) by A1, Def3;
( dom g c= proj2 (dom f) & rng g c= rng f ) by A1, A2, Th38;
hence t in PFuncs (proj2 (dom f)),(rng f) by A1, A2, PARTFUN1:def 5; :: thesis: verum

end;

let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in rng (curry' f) or t in PFuncs (proj1 (dom f)),(rng f) )
assume t in rng (curry' f) ; :: thesis: t in PFuncs (proj1 (dom f)),(rng f)
then consider z being set such that
A3: ( z in dom (curry' f) & t = (curry' f) . z ) by FUNCT_1:def 5;
( dom (curry (~ f)) = proj1 (dom (~ f)) & curry' f = curry (~ f) ) by Def3;
then consider g being Function such that
A4: ( (curry (~ f)) . z = g & dom g = proj2 ((dom (~ f)) /\ [:{z},(proj2 (dom (~ f))):]) & ( for y being set st y in dom g holds
g . y = (~ f) . z,y ) ) by A3, Def3;
( dom g c= proj2 (dom (~ f)) & rng g c= rng (~ f) & rng (~ f) c= rng f ) by A3, A4, Th38, FUNCT_4:42;
then ( dom g c= proj1 (dom f) & rng g c= rng f ) by Th20, XBOOLE_1:1;
hence t in PFuncs (proj1 (dom f)),(rng f) by A3, A4, PARTFUN1:def 5; :: thesis: verum