f in FPrg (ND (V,A)) by PARTFUN1:45;
hence (SCassignment (V,A,v)) . f is SCBinominativeFunction of V,A by PARTFUN1:46, FUNCT_2:5; :: thesis: verum