let S be Language; :: thesis: for w being string of S st w is termal holds
(rng w) /\ (LettersOf S) <> {}
let w be string of S; :: thesis: ( w is termal implies (rng w) /\ (LettersOf S) <> {} )
set L = LettersOf S;
set F = S -firstChar ;
set TT = AllTermsOf S;
set C = S -multiCat ;
set SS = AllSymbolsOf S;
set CC = (AllSymbolsOf S) -multiCat ;
set T = S -termsOfMaxDepth ;
reconsider TTT = AllTermsOf S as Subset of ((AllSymbolsOf S) *) by XBOOLE_1:1;
defpred S₁[ Nat] means for w being string of S st w is $1 -termal holds
(rng w) /\ (LettersOf S) <> {} ;
A1: S₁[ 0 ]

proof

let w be string of S; :: thesis: ( w is 0 -termal implies (rng w) /\ (LettersOf S) <> {} )
assume w is 0 -termal ; :: thesis: (rng w) /\ (LettersOf S) <> {}
then reconsider t0 = w as 0 -termal string of S ;
reconsider l = (S -firstChar) . t0 as literal Element of S ;
reconsider ll = l as Element of LettersOf S by FOMODEL1:def 14;
t0 = <*l*> ^ ((S -multiCat) . (SubTerms t0)) by FOMODEL1:def 37
.= <*l*> ^ {}
.= <*l*> ;
then (rng t0) /\ (LettersOf S) = {ll} null (LettersOf S) by FINSEQ_1:38;
hence (rng w) /\ (LettersOf S) <> {} ; :: thesis: verum

end;

A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
reconsider kk = k as Element of NAT by ORDINAL1:def 12;
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
let w be string of S; :: thesis: ( w is k + 1 -termal implies (rng w) /\ (LettersOf S) <> {} )
assume w is k + 1 -termal ; :: thesis: (rng w) /\ (LettersOf S) <> {}
then reconsider t = w as k + 1 -termal string of S ;

per cases ( not t is 0 -termal or t is 0 -termal ) ;

suppose not t is 0 -termal ; :: thesis: (rng w) /\ (LettersOf S) <> {}

then (S -firstChar) . t is operational by FOMODEL1:16;
then reconsider n = |.(ar ((S -firstChar) . t)).| as non zero Nat ;
consider m being Nat such that
A4: n = m + 1 by NAT_1:6;
reconsider mm = m, nn = n as Element of NAT by ORDINAL1:def 12;
reconsider tt = t as kk + 1 -termal string of S ;
reconsider ST = SubTerms t as m + 1 -element Element of (AllTermsOf S) * by A4;
ST is (m + 1) + 0 -element ;
then {(ST . (m + 1))} \ (AllTermsOf S) = {} ;
then reconsider q = ST . (m + 1) as Element of TTT by ZFMISC_1:60;
q is Element of (AllSymbolsOf S) * by TARSKI:def 3;
then reconsider qq = q as AllSymbolsOf S -valued FinSequence ;
reconsider p = ST | (Seg m) as TTT -valued FinSequence ;
((ST | (Seg m)) ^ <*(ST . (m + 1))*>) \+\ ST = {} ;
then A5: ST = p ^ <*qq*> by FOMODEL0:29;
A6: (S -multiCat) . ST = ((S -multiCat) . p) ^ qq by A5, FOMODEL0:33;
t = <*((S -firstChar) . t)*> ^ (((S -multiCat) . p) ^ qq) by FOMODEL1:def 37, A6;
then rng t = (rng <*((S -firstChar) . t)*>) \/ (rng (((S -multiCat) . p) ^ qq)) by FINSEQ_1:31
.= {((S -firstChar) . t)} \/ (rng (((S -multiCat) . p) ^ qq)) by FINSEQ_1:38
.= {((S -firstChar) . t)} \/ ((rng ((S -multiCat) . p)) \/ (rng qq)) by FINSEQ_1:31
.= (rng qq) \/ ({((S -firstChar) . t)} \/ (rng ((S -multiCat) . p))) by XBOOLE_1:4 ;
then (rng qq) null ({((S -firstChar) . t)} \/ (rng ((S -multiCat) . p))) c= rng t ;
then A7: (rng q) /\ (LettersOf S) c= (rng t) /\ (LettersOf S) by XBOOLE_1:26;
SubTerms tt is (S -termsOfMaxDepth) . kk -valued ;
then reconsider STT = ST as (S -termsOfMaxDepth) . kk -valued (m + 1) + 0 -element FinSequence ;
{(STT . (m + 1))} \ ((S -termsOfMaxDepth) . kk) = {} ;
then reconsider qqq = q as Element of (S -termsOfMaxDepth) . kk by ZFMISC_1:60;
reconsider tq = qqq as k -termal string of S by FOMODEL1:def 33;
(rng tq) /\ (LettersOf S) <> {} by A3;
hence (rng w) /\ (LettersOf S) <> {} by A7; :: thesis: verum

end;

suppose t is 0 -termal ; :: thesis: (rng w) /\ (LettersOf S) <> {}

hence (rng w) /\ (LettersOf S) <> {} by A1; :: thesis: verum

end;

end;

end;

A8: for m being Nat holds S₁[m] from NAT_1:sch 2(A1, A2);
assume w is termal ; :: thesis: (rng w) /\ (LettersOf S) <> {}
then reconsider t = w as termal string of S ;
t is Depth t -termal by FOMODEL1:def 40;
hence (rng w) /\ (LettersOf S) <> {} by A8; :: thesis: verum