let X, Y be set ; :: thesis: Funcs (X,Y) c= PFuncs (X,Y)
let x be object ; :: 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 3; :: thesis: verum