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

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

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;