:: deftheorem defines naming NOMIN_1:def 15 :
for V, A being set
for f being b₁ -valued FinSequence
for a being object holds naming (V,A,f,a) = (namingSeq (V,A,f,a)) . (len (namingSeq (V,A,f,a)));