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