set d = Depth phi;
set F = S -firstChar ;
set s = (S -firstChar) . phi;
set N = TheNorSymbOf S;
set dh = Depth (head phi);
reconsider h = head phi as Depth (head phi) -wff string of S by Def30;
A1: Depth phi <= m + 1 by Def30;

per cases ( phi is 0wff or ( not phi is 0wff & not phi is exal ) or ( not phi is 0wff & phi is exal ) ) ;

suppose phi is 0wff ; :: thesis: for b₁ being string of S st b₁ = head phi holds
b₁ is m -wff

then reconsider phi0 = phi as 0 -wff string of S ;
phi0 is 0 + (0 * m) -wff ;
then phi0 null phi0 is 0 + m -wff string of S ;
then head phi0 is m -wff ;
hence for b₁ being string of S st b₁ = head phi holds
b₁ is m -wff ; :: thesis: verum

end;

suppose ( not phi is 0wff & not phi is exal ) ; :: thesis: for b₁ being string of S st b₁ = head phi holds
b₁ is m -wff

then reconsider phii = phi as non 0wff m + 1 -wff non exal string of S ;
head phii is m -wff string of S by Lm39;
hence for b₁ being string of S st b₁ = head phi holds
b₁ is m -wff ; :: thesis: verum

end;

suppose ( not phi is 0wff & phi is exal ) ; :: thesis: for b₁ being string of S st b₁ = head phi holds
b₁ is m -wff

then reconsider phii = phi as non 0wff m + 1 -wff exal string of S ;
set t = tail phii;
phii = (<*((S -firstChar) . phi)*> ^ h) ^ (tail phii) by Th23
.= <*((S -firstChar) . phi)*> ^ h ;
then (Depth (head phi)) + 1 <= m + 1 by A1, Th17;
then Depth (head phi) <= m by XREAL_1:8;
then (Depth (head phi)) + (- (Depth (head phi))) <= m + (- (Depth (head phi))) by XREAL_1:6;
then reconsider n = m - (Depth (head phi)) as Nat ;
h is (Depth (head phi)) + (0 * n) -wff ;
then h is (Depth (head phi)) + n -wff ;
hence for b₁ being string of S st b₁ = head phi holds
b₁ is m -wff ; :: thesis: verum

end;

end;