let x be set ; :: according to FRAENKEL:def 1 :: thesis: ( x in PFuncs A,B implies x is Function )
assume x in PFuncs A,B ; :: thesis: x is Function
then ex f being Function st
( x = f & dom f c= A & rng f c= B ) by PARTFUN1:def 5;
hence x is Function ; :: thesis: verum