:: deftheorem Def14 defines namingSeq NOMIN_1:def 14 :
for V, A being set
for a being object
for f being b₁ -valued FinSequence st len f > 0 holds
for b₅ being FinSequence holds
( b₅ = namingSeq (V,A,f,a) iff ( len b₅ = len f & b₅ . 1 = naming (V,A,(f . (len f)),a) & ( for n being Nat st 1 <= n & n < len b₅ holds
b₅ . (n + 1) = naming (V,A,(f . ((len f) - n)),(b₅ . n)) ) ) );