let S be Language; :: thesis: for w being string of S st w is termal holds
(rng w) /\ () <> {}

let w be string of S; :: thesis: ( w is termal implies (rng w) /\ () <> {} )
set L = LettersOf S;
set F = S -firstChar ;
set TT = AllTermsOf S;
set C = S -multiCat ;
set SS = AllSymbolsOf S;
set CC = () -multiCat ;
set T = S -termsOfMaxDepth ;
reconsider TTT = AllTermsOf S as Subset of (() *) by XBOOLE_1:1;
defpred S1[ Nat] means for w being string of S st w is \$1 -termal holds
(rng w) /\ () <> {} ;
A1: S1[ 0 ]
proof
let w be string of S; :: thesis: ( w is 0 -termal implies (rng w) /\ () <> {} )
assume w is 0 -termal ; :: thesis: (rng w) /\ () <> {}
then reconsider t0 = w as 0 -termal string of S ;
reconsider l = () . t0 as literal Element of S ;
reconsider ll = l as Element of LettersOf S by FOMODEL1:def 14;
t0 = <*l*> ^ (() . (SubTerms t0)) by FOMODEL1:def 37
.= <*l*> ^ {}
.= <*l*> ;
then (rng t0) /\ () = {ll} null () by FINSEQ_1:38;
hence (rng w) /\ () <> {} ; :: thesis: verum
end;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
reconsider kk = k as Element of NAT by ORDINAL1:def 12;
assume A3: S1[k] ; :: thesis: S1[k + 1]
let w be string of S; :: thesis: ( w is k + 1 -termal implies (rng w) /\ () <> {} )
assume w is k + 1 -termal ; :: thesis: (rng w) /\ () <> {}
then reconsider t = w as k + 1 -termal string of S ;
per cases ;
suppose not t is 0 -termal ; :: thesis: (rng w) /\ () <> {}
then (S -firstChar) . t is operational by FOMODEL1:16;
then reconsider n = |.(ar (() . 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 () * by A4;
ST is (m + 1) + 0 -element ;
then {(ST . (m + 1))} \ () = {} ;
then reconsider q = ST . (m + 1) as Element of TTT by ZFMISC_1:60;
q is Element of () * 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 = (() . p) ^ qq by ;
t = <*(() . t)*> ^ ((() . p) ^ qq) by ;
then rng t = (rng <*(() . t)*>) \/ (rng ((() . p) ^ qq)) by FINSEQ_1:31
.= {(() . t)} \/ (rng ((() . p) ^ qq)) by FINSEQ_1:38
.= {(() . t)} \/ ((rng (() . p)) \/ (rng qq)) by FINSEQ_1:31
.= (rng qq) \/ ({(() . t)} \/ (rng (() . p))) by XBOOLE_1:4 ;
then (rng qq) null ({(() . t)} \/ (rng (() . p))) c= rng t ;
then A7: (rng q) /\ () c= (rng t) /\ () by XBOOLE_1:26;
SubTerms tt is () . kk -valued ;
then reconsider STT = ST as () . kk -valued (m + 1) + 0 -element FinSequence ;
{(STT . (m + 1))} \ (() . kk) = {} ;
then reconsider qqq = q as Element of () . kk by ZFMISC_1:60;
reconsider tq = qqq as k -termal string of S by FOMODEL1:def 33;
(rng tq) /\ () <> {} by A3;
hence (rng w) /\ () <> {} by A7; :: thesis: verum
end;
end;
end;
A8: for m being Nat holds S1[m] from NAT_1:sch 2(A1, A2);
assume w is termal ; :: thesis: (rng w) /\ () <> {}
then reconsider t = w as termal string of S ;
t is Depth t -termal by FOMODEL1:def 40;
hence (rng w) /\ () <> {} by A8; :: thesis: verum