let m be Nat; :: thesis: for S being Language holds (S -termsOfMaxDepth) . m c= (TermSymbolsOf S) *
let S be Language; :: thesis: (S -termsOfMaxDepth) . m c= (TermSymbolsOf S) *
set TS = TermSymbolsOf S;
set F = S -firstChar ;
set C = S -multiCat ;
set P = OpSymbolsOf S;
set T = S -termsOfMaxDepth ;
set SS = AllSymbolsOf S;
set CC = (TermSymbolsOf S) -multiCat ;
defpred S₁[ Nat] means (S -termsOfMaxDepth) . $1 c= (TermSymbolsOf S) * ;
B0: S₁[ 0 ]

proof

now

let x be set ; :: thesis: ( x in (S -termsOfMaxDepth) . 0 implies x in (TermSymbolsOf S) * )
assume x in (S -termsOfMaxDepth) . 0 ; :: thesis: x in (TermSymbolsOf S) *
then reconsider t = x as 0 -termal string of S by DefTermal;
reconsider s = (S -firstChar) . t as termal Element of S ;
set sub = SubTerms t;
reconsider ss = s as Element of TermSymbolsOf S by DefTermal0;
t = <*s*> ^ ((S -multiCat) . (SubTerms t)) by DefSubTerms1
.= <*s*> ^ {}
.= <*ss*> ;
then t is FinSequence of TermSymbolsOf S ;
hence x in (TermSymbolsOf S) * by FINSEQ_1:def 11; :: thesis: verum

end;

hence S₁[ 0 ] by TARSKI:def 3; :: thesis: verum

end;

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

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
reconsider nn = n, NN = n + 1 as Element of NAT by ORDINAL1:def 12;
assume S₁[n] ; :: thesis: S₁[n + 1]
then reconsider Tn = (S -termsOfMaxDepth) . nn as non empty Subset of ((TermSymbolsOf S) *) ;

now

let x be set ; :: thesis: ( x in (S -termsOfMaxDepth) . (n + 1) implies b₁ in (TermSymbolsOf S) * )
assume x in (S -termsOfMaxDepth) . (n + 1) ; :: thesis: b₁ in (TermSymbolsOf S) *
then x in (S -termsOfMaxDepth) . NN ;
then reconsider t = x as n + 1 -termal string of S by DefTermal;
set s = (S -firstChar) . t;
set m = abs (ar ((S -firstChar) . t));
reconsider tt = t as nn + 1 -termal string of S ;

per cases ( not t is 0 -termal or t is 0 -termal ) ;

suppose not t is 0 -termal ; :: thesis: b₁ in (TermSymbolsOf S) *

then D0: (S -firstChar) . t is operational by Th16;
then ( (S -firstChar) . t in OpSymbolsOf S & OpSymbolsOf S c= TermSymbolsOf S ) by DefOperational, Lm8;
then reconsider ss = (S -firstChar) . t as Element of TermSymbolsOf S ;
reconsider m1 = abs (ar ((S -firstChar) . t)) as non zero Nat by D0;
SubTerms tt is (S -termsOfMaxDepth) . nn -valued ;
then reconsider sub = SubTerms t as m1 + 0 -element FinSequence of Tn by FOMODEL0:26;
( sub in Tn * & Tn * c= ((TermSymbolsOf S) *) * ) by FINSEQ_1:def 11;
then reconsider subb = sub as m1 + 0 -element Element of ((TermSymbolsOf S) *) * ;
( sub is Tn -valued & Tn c= (TermSymbolsOf S) * & TermSymbolsOf S c= AllSymbolsOf S ) by XBOOLE_1:1;
then <*ss*> ^ (((TermSymbolsOf S) -multiCat) . subb) = <*((S -firstChar) . t)*> ^ ((S -multiCat) . (SubTerms t)) by FOMODEL0:53
.= t by DefSubTerms1 ;
then reconsider tt = t as FinSequence of TermSymbolsOf S by FOMODEL0:26;
tt in (TermSymbolsOf S) * by FINSEQ_1:def 11;
hence x in (TermSymbolsOf S) * ; :: thesis: verum

end;

suppose t is 0 -termal ; :: thesis: b₁ in (TermSymbolsOf S) *

then x in (S -termsOfMaxDepth) . 0 by DefTermal;
hence x in (TermSymbolsOf S) * by B0; :: thesis: verum

end;

end;

end;

hence S₁[n + 1] by TARSKI:def 3; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(B0, B1);
hence (S -termsOfMaxDepth) . m c= (TermSymbolsOf S) * ; :: thesis: verum