:: deftheorem Def40 defines + QC_LANG1:def 40 :
for A being QC-alphabet
for t being QC-symbol of A
for n being Nat
for b₄ being QC-symbol of A holds
( b₄ = t + n iff ex f being sequence of (QC-symbols A) st
( b₄ = f . n & f . 0 = t & ( for k being Nat holds f . (k + 1) = (f . k) ++ ) ) );