let X, Y be set ; :: thesis: Funcs X,Y c= PFuncs X,Y
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Funcs X,Y or x in PFuncs X,Y )
assume x in Funcs X,Y ; :: thesis: x in PFuncs X,Y
then ex f being Function st
( x = f & dom f = X & rng f c= Y ) by Def2;
hence x in PFuncs X,Y by PARTFUN1:def 5; :: thesis: verum