:: deftheorem Def9 defines SCPsuperpos NOMIN_2:def 9 :
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 [:(Pr (ND (V,A))),(product g):],(Pr (ND (V,A))) holds
( b₅ = SCPsuperpos (g,X) iff for p being SCPartialNominativePredicate of V,A
for x being Element of product g holds
( dom (b₅ . (p,x)) = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom p & d in_doms g ) } & ( for d being TypeSCNominativeData of V,A st d in_doms g holds
b₅ . (p,x),d =~ p, global_overlapping (V,A,d,(NDentry (g,X,d))) ) ) );