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