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:41;
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 object ; :: 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 object such that
A2: z in dom (curry f) and
A3: t = (curry f) . z by FUNCT_1:def 3;
dom (curry f) = proj1 (dom f) by Def1;
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 object st y in dom g holds
g . y = f . (z,y) by A2, Def1;
( dom g c= proj2 (dom f) & rng g c= rng f ) by A2, A4, Th24;
hence t in PFuncs ((proj2 (dom f)),(rng f)) by A3, A4, PARTFUN1:def 3; :: thesis: verum

end;

let t be object ; :: 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 object such that
A5: z in dom (curry' f) and
A6: t = (curry' f) . z by FUNCT_1:def 3;
dom (curry (~ f)) = proj1 (dom (~ f)) by Def1;
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 object st y in dom g holds
g . y = (~ f) . (z,y) by A5, Def1;
rng g c= rng (~ f) by A5, A7, Th24;
then A8: rng g c= rng f by A1;
dom g c= proj2 (dom (~ f)) by A5, A7, Th24;
then dom g c= proj1 (dom f) by Th11;
hence t in PFuncs ((proj1 (dom f)),(rng f)) by A6, A7, A8, PARTFUN1:def 3; :: thesis: verum