theorem Th33: :: NOMIN_2:34

for V, A being set
for d being TypeSCNominativeData of V,A
for p being SCPartialNominativePredicate of V,A
for X being Function
for g being b₁,b₂ -FPrg-yielding FinSequence st product g <> {} holds
for x being Element of product g st d in dom (SC_Psuperpos (p,x,X)) holds
( d in_doms g & (SC_Psuperpos (p,x,X)) . d = p . (global_overlapping (V,A,d,(NDentry (g,X,d)))) )