:: deftheorem Def6 defines -FPrg-yielding NOMIN_2:def 6 :
for V, A being set
for f being FinSequence holds
( f is V,A -FPrg-yielding iff for n being Nat st 1 <= n & n <= len f holds
f . n is SCBinominativeFunction of V,A );