let m be Nat; :: thesis: for S being Language
for w being string of S st w is m + 1 -wff & not w is m -wff & ( for v being literal Element of S
for phi being m -wff string of S holds not w = <*v*> ^ phi ) holds
ex phi1, phi2 being m -wff string of S st w = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2
let S be Language; :: thesis: for w being string of S st w is m + 1 -wff & not w is m -wff & ( for v being literal Element of S
for phi being m -wff string of S holds not w = <*v*> ^ phi ) holds
ex phi1, phi2 being m -wff string of S st w = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2
let w be string of S; :: thesis: ( w is m + 1 -wff & not w is m -wff & ( for v being literal Element of S
for phi being m -wff string of S holds not w = <*v*> ^ phi ) implies ex phi1, phi2 being m -wff string of S st w = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 )
set Phim = S -formulasOfMaxDepth m;
set PhiM = S -formulasOfMaxDepth (m + 1);
set L = LettersOf S;
set N = TheNorSymbOf S;
set EF = m -ExFormulasOf S;
set NF = m -NorFormulasOf S;
assume w is m + 1 -wff ; :: thesis: ( w is m -wff or 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 )
then w in S -formulasOfMaxDepth (m + 1) by DefWff1;
then w in ((m -ExFormulasOf S) \/ (m -NorFormulasOf S)) \/ (S -formulasOfMaxDepth m) by Lm37;
then B0: ( w in m -ExFormulasOf S or w in m -NorFormulasOf S or w in S -formulasOfMaxDepth m ) by Lm25;
assume Z0: not w is m -wff ; :: thesis: ( 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 )
assume B1: for v being literal Element of S
for phi being m -wff string of S holds not w = <*v*> ^ phi ; :: thesis: ex phi1, phi2 being m -wff string of S st w = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2
( w in m -ExFormulasOf S implies ex v being literal Element of S ex phi being m -wff string of S st w = <*v*> ^ phi )

proof

assume w in m -ExFormulasOf S ; :: thesis: ex v being literal Element of S ex phi being m -wff string of S st w = <*v*> ^ phi
then consider vv being Element of LettersOf S, phi being Element of S -formulasOfMaxDepth m such that
C0: w = <*vv*> ^ phi ;
reconsider phii = phi as m -wff string of S by DefWff1;
reconsider v = vv as literal Element of S ;
take v ; :: thesis: ex phi being m -wff string of S st w = <*v*> ^ phi
take phii ; :: thesis: w = <*v*> ^ phii
thus w = <*v*> ^ phii by C0; :: thesis: verum

end;

then consider phi1, phi2 being Element of S -formulasOfMaxDepth m such that
B3: w = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 by B1, Z0, B0, DefWff1;
reconsider phi11 = phi1, phi22 = phi2 as m -wff string of S by DefWff1;
take phi11 ; :: thesis: ex phi2 being m -wff string of S st w = (<*(TheNorSymbOf S)*> ^ phi11) ^ phi2
take phi22 ; :: thesis: w = (<*(TheNorSymbOf S)*> ^ phi11) ^ phi22
thus w = (<*(TheNorSymbOf S)*> ^ phi11) ^ phi22 by B3; :: thesis: verum