set F = S -firstChar ;
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;
suppose w . 1 in LettersOf S ; :: thesis: for b1 being Element of S st b1 = (S -firstChar) . w holds
not b1 is relational
then reconsider IT = (S -firstChar) . w as Element of LettersOf S by FOMODEL0:6;
not IT is relational ;
hence for b1 being Element of S st b1 = (S -firstChar) . w holds
not b1 is relational ; :: thesis: verum
end;
suppose w . 1 = TheNorSymbOf S ; :: thesis: for b1 being Element of S st b1 = (S -firstChar) . w holds
not b1 is relational
hence for b1 being Element of S st b1 = (S -firstChar) . w holds
not b1 is relational by FOMODEL0:6; :: thesis: verum
end;
end;