:: deftheorem Def14 defines SC_Fsuperpos NOMIN_2:def 14 :
for V, A being set
for f being SCBinominativeFunction of V,A
for g being b₁,b₂ -FPrg-yielding FinSequence st product g <> {} holds
for X being Function
for x being Element of product g holds SC_Fsuperpos (f,x,X) = (SCFsuperpos (g,X)) . (f,x);