set A = AllTermsOf S;
set T = S -termsOfMaxDepth ;
set Z = AtomicTermsOf S;
set SS = AllSymbolsOf S;
set s = (S -firstChar) . w;
set ss = ((AllSymbolsOf S) -firstChar) . w;
set L = LettersOf S;
w in AllTermsOf S by Def32;
then consider mm being Element of NAT such that
A1: w in (S -termsOfMaxDepth) . mm by Lm6;
reconsider ww = w as non empty FinSequence of AllSymbolsOf S by FOMODEL0:5;
A2: ((AllSymbolsOf S) -firstChar) . w = ww . 1 by FOMODEL0:6;

per cases ( mm = 0 or mm <> 0 ) ;

suppose mm = 0 ; :: thesis: for b₁ being Element of S st b₁ = (S -firstChar) . w holds
b₁ is termal

then reconsider www = w as 0 -termal string of S by Def33, A1;
(S -firstChar) . www is literal ;
hence for b₁ being Element of S st b₁ = (S -firstChar) . w holds
b₁ is termal ; :: thesis: verum

end;

suppose mm <> 0 ; :: thesis: for b₁ being Element of S st b₁ = (S -firstChar) . w holds
b₁ is termal

then consider n being Nat such that
A3: mm = n + 1 by NAT_1:6;
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
reconsider www = w as nn + 1 -termal string of S by A3, A1, Def33;
consider s1 being termal Element of S, T1 being Element of ((S -termsOfMaxDepth) . nn) * such that
A4: ( T1 is |.(ar s1).| -element & www = <*s1*> ^ ((S -multiCat) . T1) ) by Lm8;
thus for b₁ being Element of S st b₁ = (S -firstChar) . w holds
b₁ is termal by FINSEQ_1:41, A4, A2; :: thesis: verum

end;

end;