theorem :: FUNCT_5:36

for f being Function holds
( rng (curry f) c= PFuncs ((proj2 (dom f)),(rng f)) & rng (curry' f) c= PFuncs ((proj1 (dom f)),(rng f)) )