:: deftheorem Def12 defines denaming NOMIN_1:def 12 :
for V, A being set
for v being object
for D being NonatomicND of V,A st v in dom D holds
denaming (v,D) = D . v;