theorem Th37: :: NOMIN_2:38

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