( f in FPrg (ND (V,A)) & x in product g ) by A1, PARTFUN1:45;
hence (SCFsuperpos (g,X)) . (f,x) is SCBinominativeFunction of V,A by PARTFUN1:46, BINOP_1:17; :: thesis: verum