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;

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;

end;

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;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

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;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