let x be object ; :: according to FUNCT_1:def 13 :: thesis: ( not x in PFuncs (A,B) or x is set )
assume x in PFuncs (A,B) ; :: thesis: x is set
then ex f being Function st
( x = f & dom f c= A & rng f c= B ) by Def3;
hence x is set ; :: thesis: verum