let X, Y be set ; :: thesis: for B being non empty Subset of (PFuncs X,Y) holds B is non empty functional set
let B be non empty Subset of (PFuncs X,Y); :: thesis: B is non empty functional set
B is functional

proof

let x be set ; :: according to FRAENKEL:def 1 :: thesis: ( not x in B or x is set )
assume x in B ; :: thesis: x is set
hence x is Function ; :: thesis: verum

end;

hence B is non empty functional set ; :: thesis: verum