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_{1}[ Nat] means for w being string of S st w is $1 -termal holds

(rng w) /\ (LettersOf S) <> {} ;

A1: S_{1}[ 0 ]
_{1}[k] holds

S_{1}[k + 1]
_{1}[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

(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

(rng w) /\ (LettersOf S) <> {} ;

A1: S

proof

A2:
for k being Nat st S
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;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

S

proof

A8:
for m being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

reconsider kk = k as Element of NAT by ORDINAL1:def 12;

assume A3: S_{1}[k]
; :: thesis: S_{1}[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 ;

end;reconsider kk = k as Element of NAT by ORDINAL1:def 12;

assume A3: S

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 )
;

end;

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;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

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