let V, A be set ; :: thesis: NDSS (V,A) c= PFuncs (V,A)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in NDSS (V,A) or x in PFuncs (V,A) )
assume x in NDSS (V,A) ; :: thesis: x in PFuncs (V,A)
then ex w being TypeSSNominativeData of V,A st w = x ;
hence x in PFuncs (V,A) by PARTFUN1:45; :: thesis: verum