for v being object
for V, A being set
for D being NonatomicND of V,A st v in dom D holds
naming (V,A,v,(denaming (v,D))) = v .--> (D . v)