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 RELAT_1:def 19;
hence f in PFuncs X,Y by Def5; :: thesis: verum