:: deftheorem Def13 defines SCFsuperpos NOMIN_2:def 13 :
for V, A being set
for g being b₁,b₂ -FPrg-yielding FinSequence st product g <> {} holds
for X being Function
for b₅ being Function of [:(FPrg (ND (V,A))),(product g):],(FPrg (ND (V,A))) holds
( b₅ = SCFsuperpos (g,X) iff for f being SCBinominativeFunction of V,A
for x being Element of product g holds
( dom (b₅ . (f,x)) = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom f & d in_doms g ) } & ( for d being TypeSCNominativeData of V,A st d in_doms g holds
b₅ . (f,x),d =~ f, global_overlapping (V,A,d,(NDentry (g,X,d))) ) ) );