:: deftheorem defines naming NOMIN_1:def 19 :
for V, A being set
for v being object
for b₄ being Function of (ND (V,A)),(ND (V,A)) holds
( b₄ = naming (V,A,v) iff for D being TypeSCNominativeData of V,A holds b₄ . D = naming (V,A,v,D) );