theorem Th2: :: NOMIN_7:2

for v being object
for V, A being set
for z being Element of V
for d1 being NonatomicND of V,A st not V is empty & v in dom d1 holds
(local_overlapping (V,A,d1,((denaming (V,A,v)) . d1),z)) . z = d1 . v