:: deftheorem Def23 defines -tail POLNOT_1:def 23 :
for S being Polish-language
for p, b₃ being FinSequence holds
( b₃ = S -tail p iff p = (S -head p) ^ b₃ );