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)) )
A1: rng (~ f) c= rng f by FUNCT_4:42;
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
A2: z in dom (curry f) and
A3: t = (curry f) . z by FUNCT_1:def 5;
dom (curry f) = proj1 (dom f) by Def3;
then consider g being Function such that
A4: (curry f) . z = g and
dom g = proj2 ((dom f) /\ [:{z},(proj2 (dom f)):]) and
for y being set st y in dom g holds
g . y = f . (z,y) by A2, Def3;
( dom g c= proj2 (dom f) & rng g c= rng f ) by A2, A4, Th38;
hence t in PFuncs ((proj2 (dom f)),(rng f)) by A3, A4, 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
A5: z in dom (curry' f) and
A6: t = (curry' f) . z by FUNCT_1:def 5;
dom (curry (~ f)) = proj1 (dom (~ f)) by Def3;
then consider g being Function such that
A7: (curry (~ f)) . z = g and
dom g = proj2 ((dom (~ f)) /\ [:{z},(proj2 (dom (~ f))):]) and
for y being set st y in dom g holds
g . y = (~ f) . (z,y) by A5, Def3;
rng g c= rng (~ f) by A5, A7, Th38;
then A8: rng g c= rng f by A1, XBOOLE_1:1;
dom g c= proj2 (dom (~ f)) by A5, A7, Th38;
then dom g c= proj1 (dom f) by Th20;
hence t in PFuncs ((proj1 (dom f)),(rng f)) by A6, A7, A8, PARTFUN1:def 5; :: thesis: verum