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₁[ Nat] means for w being string of S st w is $1 -wff holds
(rng w) /\ (LettersOf S) <> {} ;
A1: S₁[ 0 ]

proof

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;

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

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[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 ;

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

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;

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

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

end;

end;

end;

A6: for m being Nat holds S₁[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