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 ( mmm = 0 or mmm <> 0 ) ;

suppose mmm = 0 ; :: thesis: ex b₁ being Element of (AllTermsOf S) * st
( b₁ is |.(ar ((S -firstChar) . t)).| -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . b₁) )

then reconsider ttt = tt as 0 -termal string of S ;
reconsider e = {} as Element of (AllTermsOf S) * by FINSEQ_1:49;
take e ; :: thesis: ( e is |.(ar ((S -firstChar) . t)).| -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . e) )
|.(ar ((S -firstChar) . ttt)).| is zero ;
hence e is |.(ar ((S -firstChar) . t)).| -element ; :: thesis: t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . e)
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: verum

end;

suppose mmm <> 0 ; :: thesis: ex b₁ being Element of (AllTermsOf S) * st
( b₁ is |.(ar ((S -firstChar) . t)).| -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . b₁) )

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: ( STT is |.(ar ((S -firstChar) . t)).| -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . STT) )
thus ( STT is |.(ar ((S -firstChar) . t)).| -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . STT) ) by A4; :: thesis: verum

end;

end;