set SS = AllSymbolsOf S;
set T = S -termsOfMaxDepth ;
set TT = AllTermsOf S;
set s = (S -firstChar) . t;
set n = |.(ar ((S -firstChar) . t)).|;
t in AllTermsOf S by Def32;
then consider mmm being Element of NAT such that
A1: t in (S -termsOfMaxDepth) . mmm by Lm6;
reconsider tt = t as mmm -termal string of S by A1, Def33;
reconsider tttt = t as non empty FinSequence of AllSymbolsOf S by FOMODEL0:5;

per cases ;

suppose mmm = 0 ; :: thesis:

then reconsider ttt = tt as 0 -termal string of S ;
reconsider e = {} as Element of (AllTermsOf S) * by FINSEQ_1:49;
take e ; :: thesis:
|.(ar ((S -firstChar) . ttt)).| is zero ;
hence e is |.(ar ((S -firstChar) . t)).| -element ; :: thesis:
len ttt = 1 by CARD_1:def 7;
then tttt = <*(tttt . 1)*> by FINSEQ_5:14
.= <*(((AllSymbolsOf S) -firstChar) . t)*> ^ {} by FOMODEL0:6
.= <*(((AllSymbolsOf S) -firstChar) . t)*> ^ ((S -multiCat) . e) ;
hence t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . e) ; :: thesis:

end;

suppose mmm <> 0 ; :: thesis:

then consider m being Nat such that
A3: mmm = m + 1 by NAT_1:6;
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
reconsider ttt = tt as mm + 1 -termal string of S by A3;
consider ST being Element of ((S -termsOfMaxDepth) . mm) * such that
A4: ( ST is |.(ar ((S -firstChar) . t)).| -element & ttt = <*((S -firstChar) . ttt)*> ^ ((S -multiCat) . ST) ) by Th3;
reconsider TM = (S -termsOfMaxDepth) . mm as Subset of (AllTermsOf S) by Th2;
( ST in TM * & TM * c= (AllTermsOf S) * ) ;
then reconsider STT = ST as Element of (AllTermsOf S) * ;
take STT ; :: thesis:
thus ( STT is |.(ar ((S -firstChar) . t)).| -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . STT) ) by A4; :: thesis:

end;

end;