let X, Y be set ; :: thesis: for f being PartFunc of X,Y holds f in PFuncs X,Y
let f be PartFunc of X,Y; :: thesis: f in PFuncs X,Y
( dom f c= X & rng f c= Y ) by RELSET_1:12;
hence f in PFuncs X,Y by Def5; :: thesis: verum