set SS = AllSymbolsOf S;
set T = S -termsOfMaxDepth ;
set TT = AllTermsOf S;
set s = (S -firstChar) . t;
set n = abs (ar ((S -firstChar) . t));
t in AllTermsOf S by DefTermal2;
then consider mmm being Element of NAT such that
B1: t in (S -termsOfMaxDepth) . mmm by Lm26;
reconsider tt = t as mmm -termal string of S by B1, DefTermal;
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 abs (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 abs (ar ((S -firstChar) . t)) -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . e) )
abs (ar ((S -firstChar) . ttt)) is empty ;
hence e is abs (ar ((S -firstChar) . t)) -element ; :: thesis: t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . e)
C1: len ttt = 1 by CARD_1:def 7;
then tttt = <*(tttt /. 1)*> by FINSEQ_5:14
.= <*(tttt . 1)*> by C1, FINSEQ_4:15
.= <*(((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 abs (ar ((S -firstChar) . t)) -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . b₁) )

then consider m being Nat such that
C1: 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 C1;
consider ST being Element of ((S -termsOfMaxDepth) . mm) * such that
C2: ( ST is abs (ar ((S -firstChar) . t)) -element & ttt = <*((S -firstChar) . ttt)*> ^ ((S -multiCat) . ST) ) by Lm333;
reconsider TM = (S -termsOfMaxDepth) . mm as Subset of (AllTermsOf S) by Lm4;
( ST in TM * & TM * c= (AllTermsOf S) * ) ;
then reconsider STT = ST as Element of (AllTermsOf S) * ;
take STT ; :: thesis: ( STT is abs (ar ((S -firstChar) . t)) -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . STT) )
thus ( STT is abs (ar ((S -firstChar) . t)) -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . STT) ) by C2; :: thesis: verum

end;

end;