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

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