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;
reconsider ww = w as non empty FinSequence of AllSymbolsOf S by FOMODEL0:5;
A1: ((AllSymbolsOf S) -firstChar) . w = ww . 1 by FOMODEL0:6;
w in (S -termsOfMaxDepth) . 0 by Def33;
then w in AtomicTermsOf S by Def30;
then consider x being set such that
A2: ( x in LettersOf S & w = <*x*> ) by FINSEQ_2:135;
((AllSymbolsOf S) -firstChar) . w in LettersOf S by A2, A1;
hence for b₁ being Element of S st b₁ = (S -firstChar) . w holds
b₁ is literal ; :: thesis: verum