let S be Language; :: thesis: for phi1, phi2 being wff string of S holds Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = (max ((Depth phi1),(Depth phi2))) + 1
let phi1, phi2 be wff string of S; :: thesis: Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = (max ((Depth phi1),(Depth phi2))) + 1
set nor = TheNorSymbOf S;
set phi = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2;
set m1 = Depth phi1;
set m2 = Depth phi2;
set m = max ((Depth phi1),(Depth phi2));
set M = Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2);
( Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) <= Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) & Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) > Depth phi1 & Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) > Depth phi2 ) by Lm30;
then Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) > max ((Depth phi1),(Depth phi2)) by XXREAL_0:def 10;
then B1: (max ((Depth phi1),(Depth phi2))) + 1 <= Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) by NAT_1:13;
reconsider mm = max ((Depth phi1),(Depth phi2)) as Nat by XXREAL_0:16;
reconsider d1 = (max ((Depth phi1),(Depth phi2))) - (Depth phi1), d2 = (max ((Depth phi1),(Depth phi2))) - (Depth phi2) as Nat ;
( phi1 is (Depth phi1) + (0 * d1) -wff & phi2 is (Depth phi2) + (0 * d2) -wff ) by Def30;
then ( phi1 is (Depth phi1) + d1 -wff & phi2 is (Depth phi2) + d2 -wff ) ;
then reconsider phi11 = phi1, phi22 = phi2 as max ((Depth phi1),(Depth phi2)) -wff string of S ;
J1: now :: thesis: for n being Nat st (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 is n -wff holds
n >= (max ((Depth phi1),(Depth phi2))) + 1
let n be Nat; :: thesis: ( (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 is n -wff implies n >= (max ((Depth phi1),(Depth phi2))) + 1 )
assume (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 is n -wff ; :: thesis: n >= (max ((Depth phi1),(Depth phi2))) + 1
then n >= Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) by Def30;
hence n >= (max ((Depth phi1),(Depth phi2))) + 1 by B1, XXREAL_0:2; :: thesis: verum
end;
set Phim = S -formulasOfMaxDepth mm;
set NF = mm -NorFormulasOf S;
set PhiM = S -formulasOfMaxDepth (mm + 1);
set EF = mm -ExFormulasOf S;
reconsider phi111 = phi11, phi222 = phi22 as Element of S -formulasOfMaxDepth mm by Def23;
(<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 = (<*(TheNorSymbOf S)*> ^ phi111) ^ phi222 ;
then (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 in mm -NorFormulasOf S ;
then (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 in ((mm -ExFormulasOf S) \/ (mm -NorFormulasOf S)) \/ (S -formulasOfMaxDepth mm) by Lm8;
then reconsider ITT = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 as Element of S -formulasOfMaxDepth (mm + 1) by Th9;
ITT is (max ((Depth phi1),(Depth phi2))) + 1 -wff ;
then (<*(TheNorSymbOf S)*> ^ phi11) ^ phi22 is (max ((Depth phi1),(Depth phi2))) + 1 -wff string of S ;
hence Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = (max ((Depth phi1),(Depth phi2))) + 1 by Def30, J1; :: thesis: verum