( p in Pr (ND (V,A)) & f in FPrg (ND (V,A)) ) by PARTFUN1:45;
hence (SCPsuperpos (V,A,v)) . (p,f) is SCPartialNominativePredicate of V,A by PARTFUN1:46, BINOP_1:17; :: thesis: verum