let f be PartFunc of REAL,REAL; :: thesis: for x0 being Real st f is_left_divergent_to-infty_in x0 holds
( not f is_left_divergent_to+infty_in x0 & not f is_left_convergent_in x0 )
let x0 be Real; :: thesis: ( f is_left_divergent_to-infty_in x0 implies ( not f is_left_divergent_to+infty_in x0 & not f is_left_convergent_in x0 ) )
assume A1: f is_left_divergent_to-infty_in x0 ; :: thesis: ( not f is_left_divergent_to+infty_in x0 & not f is_left_convergent_in x0 )
then consider seq being Real_Sequence such that
A2: ( seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (left_open_halfline x0) ) by Th4;
A3: f /* seq is divergent_to-infty by A1, A2, LIMFUNC2:def 3;
hence not f is_left_divergent_to+infty_in x0 by A2, Th3, LIMFUNC2:def 2; :: thesis: not f is_left_convergent_in x0
for g being Real ex seq being Real_Sequence st
( seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (left_open_halfline x0) & not ( f /* seq is convergent & lim (f /* seq) = g ) ) by A2, A3, Th3;
hence not f is_left_convergent_in x0 by LIMFUNC2:def 1; :: thesis: verum