p in Pr (ND (V,A)) by PARTFUN1:45;
hence (SCexists (V,A,v)) . p is SCPartialNominativePredicate of V,A by PARTFUN1:46, FUNCT_2:5; :: thesis: verum