set L = LettersOf S;

set Phim = S -formulasOfMaxDepth m;

set NF = m -NorFormulasOf S;

set PhiM = S -formulasOfMaxDepth (m + 1);

set EF = m -ExFormulasOf S;

set IT = <*v*> ^ phi;

reconsider vv = v as Element of LettersOf S by FOMODEL1:def 14;

reconsider phii = phi as Element of S -formulasOfMaxDepth m by Def23;

<*v*> ^ phi = <*vv*> ^ phii ;

then <*v*> ^ phi in m -ExFormulasOf S ;

then <*v*> ^ phi in ((m -ExFormulasOf S) \/ (m -NorFormulasOf S)) \/ (S -formulasOfMaxDepth m) by Lm8;

then reconsider ITT = <*v*> ^ phi as Element of S -formulasOfMaxDepth (m + 1) by Th9;

ITT is m + 1 -wff ;

hence for b_{1} being string of S st b_{1} = <*v*> ^ phi holds

b_{1} is m + 1 -wff
; :: thesis: verum

set Phim = S -formulasOfMaxDepth m;

set NF = m -NorFormulasOf S;

set PhiM = S -formulasOfMaxDepth (m + 1);

set EF = m -ExFormulasOf S;

set IT = <*v*> ^ phi;

reconsider vv = v as Element of LettersOf S by FOMODEL1:def 14;

reconsider phii = phi as Element of S -formulasOfMaxDepth m by Def23;

<*v*> ^ phi = <*vv*> ^ phii ;

then <*v*> ^ phi in m -ExFormulasOf S ;

then <*v*> ^ phi in ((m -ExFormulasOf S) \/ (m -NorFormulasOf S)) \/ (S -formulasOfMaxDepth m) by Lm8;

then reconsider ITT = <*v*> ^ phi as Element of S -formulasOfMaxDepth (m + 1) by Th9;

ITT is m + 1 -wff ;

hence for b

b