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

let w be string of S; :: thesis: ( w is wff 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 -wff holds
(rng w) /\ () <> {} ;
A1: S1[ 0 ]
proof
let w be string of S; :: thesis: ( w is 0 -wff implies (rng w) /\ () <> {} )
assume w is 0 -wff ; :: thesis: (rng w) /\ () <> {}
then reconsider phi0 = w as 0wff string of S ;
reconsider r = () . 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 () * by A2;
reconsider p = ST | (Seg m) as () * -valued FinSequence ;
{(ST . (m + 1))} \ () = {} ;
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*> ^ (() . ST) by FOMODEL1:def 38
.= <*r*> ^ ((() . p) ^ qq) by ;
then rng phi0 = () \/ (rng ((() . p) ^ q)) by FINSEQ_1:31
.= () \/ ((rng (() . p)) \/ (rng q)) by FINSEQ_1:31
.= (rng q) \/ (() \/ (rng (() . p))) by XBOOLE_1:4 ;
then (rng t) null (() \/ (rng (() . p))) c= rng phi0 ;
then (rng t) /\ () c= (rng phi0) /\ () by XBOOLE_1:26;
hence (rng w) /\ () <> {} ; :: thesis: verum
end;
A4: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A5: S1[k] ; :: thesis: S1[k + 1]
let w be string of S; :: thesis: ( w is k + 1 -wff implies (rng w) /\ () <> {} )
assume w is k + 1 -wff ; :: thesis: (rng w) /\ () <> {}
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) /\ () <> {}
then reconsider phii = phi as non 0wff wff string of S ;
reconsider phi1 = head phii as k -wff string of S ;
phii = (<*(() . phii)*> ^ phi1) ^ (tail phi) by Th23;
then rng phii = (rng (<*(() . phii)*> ^ phi1)) \/ (rng (tail phi)) by FINSEQ_1:31
.= ((rng phi1) \/ (rng <*(() . phii)*>)) \/ (rng (tail phi)) by FINSEQ_1:31
.= (rng phi1) \/ ((rng <*(() . phii)*>) \/ (rng (tail phi))) by XBOOLE_1:4 ;
then (rng phi1) null ((rng <*(() . phii)*>) \/ (rng (tail phi))) c= rng phii ;
then (rng phi1) /\ () c= (rng phii) /\ () by XBOOLE_1:26;
hence (rng w) /\ () <> {} by ; :: thesis: verum
end;
end;
end;
A6: for m being Nat holds S1[m] from NAT_1:sch 2(A1, A4);
assume w is wff ; :: thesis: (rng w) /\ () <> {}
then reconsider phi = w as wff string of S ;
phi is Depth phi -wff by Def30;
hence (rng w) /\ () <> {} by A6; :: thesis: verum