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) * ;
A1: S₁[ 0 ]

proof

now :: thesis: for x being object st x in (S -termsOfMaxDepth) . 0 holds
x in (TermSymbolsOf S) *

let x be object ; :: 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 Def33;
reconsider s = (S -firstChar) . t as termal Element of S ;
set sub = SubTerms t;
reconsider ss = s as Element of TermSymbolsOf S by Def18;
t = <*s*> ^ ((S -multiCat) . (SubTerms t)) by Def37
.= <*s*> ^ {}
.= <*ss*> ;
then t is FinSequence of TermSymbolsOf S ;
hence x in (TermSymbolsOf S) * ; :: thesis: verum

end;

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

end;

A2: 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 :: thesis: for x being object st x in (S -termsOfMaxDepth) . (n + 1) holds
x in (TermSymbolsOf S) *

let x be object ; :: 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 Def33;
set s = (S -firstChar) . t;
set m = |.(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 A3: not t is 0 -termal ; :: thesis: b₁ in (TermSymbolsOf S) *

then A4: (S -firstChar) . t is operational by Th16;
( (S -firstChar) . t in OpSymbolsOf S & OpSymbolsOf S c= TermSymbolsOf S ) by Def16, Th1, Th16, A3;
then reconsider ss = (S -firstChar) . t as Element of TermSymbolsOf S ;
reconsider m1 = |.(ar ((S -firstChar) . t)).| as non zero Nat by A4;
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) *) * ) ;
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 Def37 ;
then reconsider tt = t as FinSequence of TermSymbolsOf S by FOMODEL0:26;
tt in (TermSymbolsOf S) * ;
hence x in (TermSymbolsOf S) * ; :: thesis: verum

end;

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

then x in (S -termsOfMaxDepth) . 0 ;
hence x in (TermSymbolsOf S) * by A1; :: 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(A1, A2);
hence (S -termsOfMaxDepth) . m c= (TermSymbolsOf S) * ; :: thesis: verum