( p in Pr (ND (V,A)) & x in product g ) by A1, PARTFUN1:45;
hence (SCPsuperpos (g,X)) . (p,x) is SCPartialNominativePredicate of V,A by PARTFUN1:46, BINOP_1:17; :: thesis: verum