let x0 be Real; :: thesis: for f being PartFunc of REAL ,REAL st f is_convergent_in x0 & lim f,x0 = 0 & ex r being Real st
( 0 < r & ( for g being Real st g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds
f . g < 0 ) ) holds
f ^ is_divergent_to-infty_in x0
let f be PartFunc of REAL ,REAL ; :: thesis: ( f is_convergent_in x0 & lim f,x0 = 0 & ex r being Real st
( 0 < r & ( for g being Real st g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds
f . g < 0 ) ) implies f ^ is_divergent_to-infty_in x0 )
assume that
A1: f is_convergent_in x0 and
A2: lim f,x0 = 0 ; :: thesis: ( for r being Real holds
( not 0 < r or ex g being Real st
( g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) & not f . g < 0 ) ) or f ^ is_divergent_to-infty_in x0 )
A3: f is_right_convergent_in x0 by A1, Th33;
given r being Real such that A4: 0 < r and
A5: for g being Real st g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds
f . g < 0 ; :: thesis: f ^ is_divergent_to-infty_in x0

A6: now

let g be Real; :: thesis: ( g in (dom f) /\ ].x0,(x0 + r).[ implies f . g < 0 )
assume A7: g in (dom f) /\ ].x0,(x0 + r).[ ; :: thesis: f . g < 0
then g in ].x0,(x0 + r).[ by XBOOLE_0:def 4;
then A8: g in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ by XBOOLE_0:def 3;
g in dom f by A7, XBOOLE_0:def 4;
then g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) by A8, XBOOLE_0:def 4;
hence f . g < 0 by A5; :: thesis: verum

end;

A9: now

let g be Real; :: thesis: ( g in (dom f) /\ ].(x0 - r),x0.[ implies f . g < 0 )
assume A10: g in (dom f) /\ ].(x0 - r),x0.[ ; :: thesis: f . g < 0
then g in ].(x0 - r),x0.[ by XBOOLE_0:def 4;
then A11: g in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ by XBOOLE_0:def 3;
g in dom f by A10, XBOOLE_0:def 4;
then g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) by A11, XBOOLE_0:def 4;
hence f . g < 0 by A5; :: thesis: verum

end;

lim_right f,x0 = 0 by A1, A2, Th33;
then A12: f ^ is_right_divergent_to-infty_in x0 by A3, A4, A6, LIMFUNC2:82;
A13: f is_left_convergent_in x0 by A1, Th33;
lim_left f,x0 = 0 by A1, A2, Th33;
then f ^ is_left_divergent_to-infty_in x0 by A13, A4, A9, LIMFUNC2:80;
hence f ^ is_divergent_to-infty_in x0 by A12, Th16; :: thesis: verum