let S be Language; :: thesis: for w being string of S st w is wff & not w is 0wff & not w . 1 in LettersOf S holds
w . 1 = TheNorSymbOf S
let w be string of S; :: thesis: ( w is wff & not w is 0wff & not w . 1 in LettersOf S implies w . 1 = TheNorSymbOf S )
set L = LettersOf S;
set N = TheNorSymbOf S;
set SS = AllSymbolsOf S;
assume w is wff ; :: thesis: ( w is 0wff or w . 1 in LettersOf S or w . 1 = TheNorSymbOf S )
then reconsider ww = w as wff string of S ;
set n = Depth ww;
assume not w is 0wff ; :: thesis: ( w . 1 in LettersOf S or w . 1 = TheNorSymbOf S )
then consider m being Nat such that
A1: Depth ww = m + 1 by NAT_1:6;
m + 1 > m + 0 by XREAL_1:8;
then ( ww is m + 1 -wff & not ww is m -wff ) by Def30, A1;
per cases then ( ex v being literal Element of S ex phi being m -wff string of S st w = <*v*> ^ phi or ex phi1, phi2 being m -wff string of S st w = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 ) by Lm21;
suppose ex v being literal Element of S ex phi being m -wff string of S st w = <*v*> ^ phi ; :: thesis: ( w . 1 in LettersOf S or w . 1 = TheNorSymbOf S )
then consider v being literal Element of S, phi being m -wff string of S such that
A2: w = <*v*> ^ phi ;
v = w . 1 by A2, FINSEQ_1:41;
hence ( w . 1 in LettersOf S or w . 1 = TheNorSymbOf S ) by FOMODEL1:def 14; :: thesis: verum
end;
suppose ex phi1, phi2 being m -wff string of S st w = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 ; :: thesis: ( w . 1 in LettersOf S or w . 1 = TheNorSymbOf S )
then consider phi1, phi2 being m -wff string of S such that
A3: w = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 ;
w . 1 = (<*(TheNorSymbOf S)*> ^ (phi1 ^ phi2)) . 1 by A3, FINSEQ_1:32
.= TheNorSymbOf S by FINSEQ_1:41 ;
hence ( w . 1 in LettersOf S or w . 1 = TheNorSymbOf S ) ; :: thesis: verum
end;
end;