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;

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 ) )
;

end;

suppose
phi is 0wff
; :: thesis: for b_{1} being string of S st b_{1} = head phi holds

b_{1} is m -wff

b

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_{1} being string of S st b_{1} = head phi holds

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

end;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

b

suppose
( not phi is 0wff & not phi is exal )
; :: thesis: for b_{1} being string of S st b_{1} = head phi holds

b_{1} is m -wff

b

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_{1} being string of S st b_{1} = head phi holds

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

end;head phii is m -wff string of S by Lm39;

hence for b

b

suppose
( not phi is 0wff & phi is exal )
; :: thesis: for b_{1} being string of S st b_{1} = head phi holds

b_{1} is m -wff

b

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_{1} being string of S st b_{1} = head phi holds

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

end;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

b