per cases ( n <= len p or len p <= n ) ;

suppose n <= len p ; :: thesis: not p | n is empty

then (n + 1) - 1 <= (len p) - 0 ;
then len (p | n) = n by Th59;
hence not p | n is empty ; :: thesis: verum

end;

suppose len p <= n ; :: thesis: not p | n is empty

hence not p | n is empty by Th58; :: thesis: verum

end;

end;