:: deftheorem Def11 defines SCPsuperpos NOMIN_2:def 11 :
for V, A being set
for v being object
for b₄ being Function of [:(Pr (ND (V,A))),(FPrg (ND (V,A))):],(Pr (ND (V,A))) holds
( b₄ = SCPsuperpos (V,A,v) iff for p being SCPartialNominativePredicate of V,A
for f being SCBinominativeFunction of V,A holds
( dom (b₄ . (p,f)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(f . d),v) in dom p & d in dom f ) } & ( for d being TypeSCNominativeData of V,A st d in dom f holds
b₄ . (p,f),d =~ p, local_overlapping (V,A,d,(f . d),v) ) ) );