for T being Polish-language
for A being Polish-arity-function of T
for n being Nat
for F being Element of Polish-expression-hierarchy (T,A,(n + 1)) holds T -tail F in (Polish-expression-hierarchy (T,A,n)) ^^ (Polish-arity F)