let S be Language; :: thesis: for w being string of S st w is wff holds

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

let w be string of S; :: thesis: ( w is wff 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 -wff holds

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

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

S_{1}[k + 1]
_{1}[m]
from NAT_1:sch 2(A1, A4);

assume w is wff ; :: thesis: (rng w) /\ (LettersOf S) <> {}

then reconsider phi = w as wff string of S ;

phi is Depth phi -wff by Def30;

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

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

let w be string of S; :: thesis: ( w is wff 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

A4:
for k being Nat st S
let w be string of S; :: thesis: ( w is 0 -wff implies (rng w) /\ (LettersOf S) <> {} )

assume w is 0 -wff ; :: thesis: (rng w) /\ (LettersOf S) <> {}

then reconsider phi0 = w as 0wff string of S ;

reconsider r = (S -firstChar) . phi0 as relational Element of S ;

reconsider n = |.(ar r).| as non zero Nat ;

consider m being Nat such that

A2: n = m + 1 by NAT_1:6;

reconsider ST = SubTerms phi0 as (m + 1) + 0 -element Element of (AllTermsOf S) * by A2;

reconsider p = ST | (Seg m) as (AllSymbolsOf S) * -valued FinSequence ;

{(ST . (m + 1))} \ (AllTermsOf S) = {} ;

then reconsider q = ST . (m + 1) as Element of AllTermsOf S by ZFMISC_1:60;

reconsider t = q as termal string of S ;

((ST | (Seg m)) ^ <*q*>) \+\ ST = {} ;

then A3: ST = (ST | (Seg m)) ^ <*q*> by FOMODEL0:29;

reconsider qq = q as AllSymbolsOf S -valued FinSequence ;

phi0 = <*r*> ^ ((S -multiCat) . ST) by FOMODEL1:def 38

.= <*r*> ^ (((S -multiCat) . p) ^ qq) by A3, FOMODEL0:33 ;

then rng phi0 = (rng <*r*>) \/ (rng (((S -multiCat) . p) ^ q)) by FINSEQ_1:31

.= (rng <*r*>) \/ ((rng ((S -multiCat) . p)) \/ (rng q)) by FINSEQ_1:31

.= (rng q) \/ ((rng <*r*>) \/ (rng ((S -multiCat) . p))) by XBOOLE_1:4 ;

then (rng t) null ((rng <*r*>) \/ (rng ((S -multiCat) . p))) c= rng phi0 ;

then (rng t) /\ (LettersOf S) c= (rng phi0) /\ (LettersOf S) by XBOOLE_1:26;

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

end;assume w is 0 -wff ; :: thesis: (rng w) /\ (LettersOf S) <> {}

then reconsider phi0 = w as 0wff string of S ;

reconsider r = (S -firstChar) . phi0 as relational Element of S ;

reconsider n = |.(ar r).| as non zero Nat ;

consider m being Nat such that

A2: n = m + 1 by NAT_1:6;

reconsider ST = SubTerms phi0 as (m + 1) + 0 -element Element of (AllTermsOf S) * by A2;

reconsider p = ST | (Seg m) as (AllSymbolsOf S) * -valued FinSequence ;

{(ST . (m + 1))} \ (AllTermsOf S) = {} ;

then reconsider q = ST . (m + 1) as Element of AllTermsOf S by ZFMISC_1:60;

reconsider t = q as termal string of S ;

((ST | (Seg m)) ^ <*q*>) \+\ ST = {} ;

then A3: ST = (ST | (Seg m)) ^ <*q*> by FOMODEL0:29;

reconsider qq = q as AllSymbolsOf S -valued FinSequence ;

phi0 = <*r*> ^ ((S -multiCat) . ST) by FOMODEL1:def 38

.= <*r*> ^ (((S -multiCat) . p) ^ qq) by A3, FOMODEL0:33 ;

then rng phi0 = (rng <*r*>) \/ (rng (((S -multiCat) . p) ^ q)) by FINSEQ_1:31

.= (rng <*r*>) \/ ((rng ((S -multiCat) . p)) \/ (rng q)) by FINSEQ_1:31

.= (rng q) \/ ((rng <*r*>) \/ (rng ((S -multiCat) . p))) by XBOOLE_1:4 ;

then (rng t) null ((rng <*r*>) \/ (rng ((S -multiCat) . p))) c= rng phi0 ;

then (rng t) /\ (LettersOf S) c= (rng phi0) /\ (LettersOf S) by XBOOLE_1:26;

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

S

proof

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

assume A5: S_{1}[k]
; :: thesis: S_{1}[k + 1]

let w be string of S; :: thesis: ( w is k + 1 -wff implies (rng w) /\ (LettersOf S) <> {} )

assume w is k + 1 -wff ; :: thesis: (rng w) /\ (LettersOf S) <> {}

then reconsider phi = w as k + 1 -wff string of S ;

end;assume A5: S

let w be string of S; :: thesis: ( w is k + 1 -wff implies (rng w) /\ (LettersOf S) <> {} )

assume w is k + 1 -wff ; :: thesis: (rng w) /\ (LettersOf S) <> {}

then reconsider phi = w as k + 1 -wff string of S ;

per cases
( not phi is 0wff or phi is 0wff )
;

end;

suppose
not phi is 0wff
; :: thesis: (rng w) /\ (LettersOf S) <> {}

then reconsider phii = phi as non 0wff wff string of S ;

reconsider phi1 = head phii as k -wff string of S ;

phii = (<*((S -firstChar) . phii)*> ^ phi1) ^ (tail phi) by Th23;

then rng phii = (rng (<*((S -firstChar) . phii)*> ^ phi1)) \/ (rng (tail phi)) by FINSEQ_1:31

.= ((rng phi1) \/ (rng <*((S -firstChar) . phii)*>)) \/ (rng (tail phi)) by FINSEQ_1:31

.= (rng phi1) \/ ((rng <*((S -firstChar) . phii)*>) \/ (rng (tail phi))) by XBOOLE_1:4 ;

then (rng phi1) null ((rng <*((S -firstChar) . phii)*>) \/ (rng (tail phi))) c= rng phii ;

then (rng phi1) /\ (LettersOf S) c= (rng phii) /\ (LettersOf S) by XBOOLE_1:26;

hence (rng w) /\ (LettersOf S) <> {} by A5, XBOOLE_1:3; :: thesis: verum

end;reconsider phi1 = head phii as k -wff string of S ;

phii = (<*((S -firstChar) . phii)*> ^ phi1) ^ (tail phi) by Th23;

then rng phii = (rng (<*((S -firstChar) . phii)*> ^ phi1)) \/ (rng (tail phi)) by FINSEQ_1:31

.= ((rng phi1) \/ (rng <*((S -firstChar) . phii)*>)) \/ (rng (tail phi)) by FINSEQ_1:31

.= (rng phi1) \/ ((rng <*((S -firstChar) . phii)*>) \/ (rng (tail phi))) by XBOOLE_1:4 ;

then (rng phi1) null ((rng <*((S -firstChar) . phii)*>) \/ (rng (tail phi))) c= rng phii ;

then (rng phi1) /\ (LettersOf S) c= (rng phii) /\ (LettersOf S) by XBOOLE_1:26;

hence (rng w) /\ (LettersOf S) <> {} by A5, XBOOLE_1:3; :: thesis: verum

assume w is wff ; :: thesis: (rng w) /\ (LettersOf S) <> {}

then reconsider phi = w as wff string of S ;

phi is Depth phi -wff by Def30;

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