set N = TheNorSymbOf S;
set Phim = S -formulasOfMaxDepth m;
set NF = m -NorFormulasOf S;
set PhiM = S -formulasOfMaxDepth (m + 1);
set EF = m -ExFormulasOf S;
set IT = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2;
reconsider phi11 = phi1, phi22 = phi2 as Element of S -formulasOfMaxDepth m by Def23;
(<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 = (<*(TheNorSymbOf S)*> ^ phi11) ^ phi22 ;
then (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 in m -NorFormulasOf S ;
then (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 in ((m -ExFormulasOf S) \/ (m -NorFormulasOf S)) \/ (S -formulasOfMaxDepth m) by Lm8;
then reconsider ITT = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 as Element of S -formulasOfMaxDepth (m + 1) by Th9;
ITT is m + 1 -wff ;
hence for b₁ being string of S st b₁ = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 holds
b₁ is m + 1 -wff ; :: thesis: verum