let T be Polish-language; :: thesis: 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)
let A be Polish-arity-function of T; :: thesis: 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)
let n be Nat; :: thesis: 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)
let F be Element of Polish-expression-hierarchy (T,A,(n + 1)); :: thesis: T -tail F in (Polish-expression-hierarchy (T,A,n)) ^^ (Polish-arity F)
set U = Polish-expression-hierarchy (T,A,n);
F in Polish-expression-hierarchy (T,A,(n + 1)) ;
then F in Polish-expression-layer (T,A,(Polish-expression-hierarchy (T,A,n))) by Th23;
then consider t being Element of T, u being Element of T * such that
A2: F = t ^ u and
A3: u in (Polish-expression-hierarchy (T,A,n)) ^^ (A . t) by Def19;
thus T -tail F in (Polish-expression-hierarchy (T,A,n)) ^^ (Polish-arity F) by A2, A3; :: thesis: verum