let m be Nat; :: thesis: for S being Language
for phi being wff string of S st not phi is 0wff & not phi is exal & phi is m + 1 -wff holds
( head phi is m -wff string of S & tail phi is m -wff string of S )
let S be Language; :: thesis: for phi being wff string of S st not phi is 0wff & not phi is exal & phi is m + 1 -wff holds
( head phi is m -wff string of S & tail phi is m -wff string of S )
let phi be wff string of S; :: thesis: ( not phi is 0wff & not phi is exal & phi is m + 1 -wff implies ( head phi is m -wff string of S & tail phi is m -wff string of S ) )
assume ( not phi is 0wff & not phi is exal & phi is m + 1 -wff ) ; :: thesis: ( head phi is m -wff string of S & tail phi is m -wff string of S )
then reconsider phii = phi as non 0wff m + 1 -wff non exal string of S ;
set N = TheNorSymbOf S;
set F = S -firstChar ;
set s = (S -firstChar) . phii;
set dh = Depth (head phii);
set dt = Depth (tail phii);
set M = max ((Depth (head phii)),(Depth (tail phii)));
set d = Depth phii;
reconsider h = head phii as Depth (head phii) -wff string of S by Def30;
reconsider t = tail phii as Depth (tail phii) -wff string of S by Def30;
A1: Depth phii <= m + 1 by Def30;
((S -firstChar) . phii) \+\ (TheNorSymbOf S) = {} ;
then (S -firstChar) . phii = TheNorSymbOf S by FOMODEL0:29;
then phii = (<*(TheNorSymbOf S)*> ^ h) ^ t by Th23;
then (max ((Depth (head phii)),(Depth (tail phii)))) + 1 <= m + 1 by A1, Th17;
then ((max ((Depth (head phii)),(Depth (tail phii)))) + 1) - 1 <= (m + 1) - 1 by XREAL_1:8;
then ( (max ((Depth (head phii)),(Depth (tail phii)))) + (- (Depth (head phii))) <= m + (- (Depth (head phii))) & (max ((Depth (head phii)),(Depth (tail phii)))) + (- (Depth (tail phii))) <= m + (- (Depth (tail phii))) ) by XREAL_1:6;
then ( (max ((Depth (head phii)),(Depth (tail phii)))) - (Depth (head phii)) <= m - (Depth (head phii)) & (max ((Depth (head phii)),(Depth (tail phii)))) - (Depth (tail phii)) <= m - (Depth (tail phii)) ) ;
then ( 0 <= m - (Depth (head phii)) & 0 <= m - (Depth (tail phii)) ) ;
then reconsider nh = m - (Depth (head phii)), nt = m - (Depth (tail phii)) as Nat ;
( h is (Depth (head phii)) + (0 * nh) -wff & t is (Depth (tail phii)) + (0 * nt) -wff ) ;
then ( h is (Depth (head phii)) + nh -wff & t is (Depth (tail phii)) + nt -wff ) ;
hence ( head phi is m -wff string of S & tail phi is m -wff string of S ) ; :: thesis: verum