:: deftheorem defines denaming NOMIN_1:def 18 :
for V, A being set
for v being object
for b₄ being PartFunc of (ND (V,A)),(ND (V,A)) holds
( b₄ = denaming (V,A,v) iff ( dom b₄ = { d where d is NonatomicND of V,A : v in dom d } & ( for D being NonatomicND of V,A st D in dom b₄ holds
b₄ . D = denaming (v,D) ) ) );