let T be Polish-language; 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; 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; 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, Th17;
hence
T -tail F in (Polish-WFF-set (T,A)) ^^ (Polish-arity F)
by A2, A3; verum