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;
B1: ((AllSymbolsOf S) -firstChar) . w = ww . 1 by FOMODEL0:6;
w in (S -termsOfMaxDepth) . 0 by DefTermal;
then w in AtomicTermsOf S by DefTerm;
then consider x being set such that
C1: ( x in LettersOf S & w = <*x*> ) by FINSEQ_2:135;
w = <*x*> ^ {} by C1;
then ((AllSymbolsOf S) -firstChar) . w in LettersOf S by C1, B1, FINSEQ_1:41;
hence for b₁ being Element of S st b₁ = (S -firstChar) . w holds
b₁ is literal by DefLiteral; :: thesis: verum