let m be Nat; :: thesis: for S being Language holds (S -termsOfMaxDepth) . m c= ((AllSymbolsOf S) *) \ {{}}
let S be Language; :: thesis: (S -termsOfMaxDepth) . m c= ((AllSymbolsOf S) *) \ {{}}
set T = S -termsOfMaxDepth ;
set SS = AllSymbolsOf S;
set L = LettersOf S;
defpred S₁[ Nat] means (S -termsOfMaxDepth) . $1 c= ((AllSymbolsOf S) *) \ {{}};
A1: S₁[ 0 ]

proof

(S -termsOfMaxDepth) . 0 = AtomicTermsOf S by Def30
.= (0 + 1) -tuples_on (LettersOf S) ;
then A2: (S -termsOfMaxDepth) . 0 c= ((LettersOf S) *) \ {{}} by FOMODEL0:9;
((LettersOf S) *) \ {{}} c= ((AllSymbolsOf S) *) \ {{}} by XBOOLE_1:33;
hence S₁[ 0 ] by A2, XBOOLE_1:1; :: thesis: verum

end;

A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
set TM1 = { (Compound (s,((S -termsOfMaxDepth) . n))) where s is ofAtomicFormula Element of S : s is operational } ;

now :: thesis: for X being set st X in { (Compound (s,((S -termsOfMaxDepth) . n))) where s is ofAtomicFormula Element of S : s is operational } holds
X c= ((AllSymbolsOf S) *) \ {{}}

let X be set ; :: thesis: ( X in { (Compound (s,((S -termsOfMaxDepth) . n))) where s is ofAtomicFormula Element of S : s is operational } implies X c= ((AllSymbolsOf S) *) \ {{}} )
assume X in { (Compound (s,((S -termsOfMaxDepth) . n))) where s is ofAtomicFormula Element of S : s is operational } ; :: thesis: X c= ((AllSymbolsOf S) *) \ {{}}
then consider s being ofAtomicFormula Element of S such that
A5: ( X = Compound (s,((S -termsOfMaxDepth) . n)) & s is operational ) ;
thus X c= ((AllSymbolsOf S) *) \ {{}} by A5; :: thesis: verum

end;

then ( union { (Compound (s,((S -termsOfMaxDepth) . n))) where s is ofAtomicFormula Element of S : s is operational } c= ((AllSymbolsOf S) *) \ {{}} & (S -termsOfMaxDepth) . (n + 1) = (union { (Compound (s,((S -termsOfMaxDepth) . n))) where s is ofAtomicFormula Element of S : s is operational } ) \/ ((S -termsOfMaxDepth) . n) ) by Def30, ZFMISC_1:76;
hence S₁[n + 1] by A4, XBOOLE_1:8; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A3);
hence (S -termsOfMaxDepth) . m c= ((AllSymbolsOf S) *) \ {{}} ; :: thesis: verum