theorem Th36: :: NOMIN_2:37

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