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