theorem Th34: :: NOMIN_2:35

for v being object
for V, A being set
for d being TypeSCNominativeData of V,A
for p being SCPartialNominativePredicate of V,A
for f being SCBinominativeFunction of V,A st d in dom (SC_Psuperpos (p,f,v)) holds
( (SC_Psuperpos (p,f,v)) . d = p . (local_overlapping (V,A,d,(f . d),v)) & d in dom f )