let T be Polish-language; :: thesis: for A being Polish-arity-function of T
for F being Polish-WFF of T,A holds T -tail F in (Polish-WFF-set (T,A)) ^^ (Polish-arity F)
let A be Polish-arity-function of T; :: thesis: for F being Polish-WFF of T,A holds T -tail F in (Polish-WFF-set (T,A)) ^^ (Polish-arity F)
let F be Polish-WFF of T,A; :: thesis: T -tail F in (Polish-WFF-set (T,A)) ^^ (Polish-arity F)
consider n being Nat, t, u being FinSequence such that
A1: t in T and
A2: n = A . t and
A3: u in (Polish-WFF-set (T,A)) ^^ n and
A4: F = t ^ u by Th32;
( T -head F = t & T -tail F = u ) by A1, A4, Th52;
hence T -tail F in (Polish-WFF-set (T,A)) ^^ (Polish-arity F) by A2, A3; :: thesis: verum