let X, Y, f be set ; :: thesis: ( f in PFuncs (X,Y) implies f is PartFunc of X,Y )
assume f in PFuncs (X,Y) ; :: thesis: f is PartFunc of X,Y
then ex F being Function st
( f = F & dom F c= X & rng F c= Y ) by Def3;
hence f is PartFunc of X,Y by RELSET_1:4; :: thesis: verum