set F = S -firstChar ;

set L = LettersOf S;

set N = TheNorSymbOf S;

set SS = AllSymbolsOf S;

set L = LettersOf S;

set N = TheNorSymbOf S;

set SS = AllSymbolsOf S;

per cases
( w . 1 in LettersOf S or w . 1 = TheNorSymbOf S )
by Lm23;

end;

suppose
w . 1 in LettersOf S
; :: thesis: for b_{1} being Element of S st b_{1} = (S -firstChar) . w holds

not b_{1} is relational

not b

then reconsider IT = (S -firstChar) . w as Element of LettersOf S by FOMODEL0:6;

not IT is relational ;

hence for b_{1} being Element of S st b_{1} = (S -firstChar) . w holds

not b_{1} is relational
; :: thesis: verum

end;not IT is relational ;

hence for b

not b

suppose
w . 1 = TheNorSymbOf S
; :: thesis: for b_{1} being Element of S st b_{1} = (S -firstChar) . w holds

not b_{1} is relational

not b

hence
for b_{1} being Element of S st b_{1} = (S -firstChar) . w holds

not b_{1} is relational
by FOMODEL0:6; :: thesis: verum

end;not b