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 Def3; :: thesis: verum