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
0 < f . g ) ) 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
0 < f . g ) ) 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 0 < f . g ) ) or f ^ is_divergent_to+infty_in x0 )
A3: f is_right_convergent_in x0 by A1, Th29;
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
0 < f . g ; :: thesis: f ^ is_divergent_to+infty_in x0

A6: now :: thesis: for g being Real st g in (dom f) /\ ].x0,(x0 + r).[ holds
0 < f . g

let g be Real; :: thesis: ( g in (dom f) /\ ].x0,(x0 + r).[ implies 0 < f . g )
assume A7: g in (dom f) /\ ].x0,(x0 + r).[ ; :: thesis: 0 < f . g
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 0 < f . g by A5; :: thesis: verum

end;

A9: now :: thesis: for g being Real st g in (dom f) /\ ].(x0 - r),x0.[ holds
0 < f . g

let g be Real; :: thesis: ( g in (dom f) /\ ].(x0 - r),x0.[ implies 0 < f . g )
assume A10: g in (dom f) /\ ].(x0 - r),x0.[ ; :: thesis: 0 < f . g
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 0 < f . g by A5; :: thesis: verum

end;

lim_right (f,x0) = 0 by A1, A2, Th29;
then A12: f ^ is_right_divergent_to+infty_in x0 by A3, A4, A6, LIMFUNC2:73;
A13: f is_left_convergent_in x0 by A1, Th29;
lim_left (f,x0) = 0 by A1, A2, Th29;
then f ^ is_left_divergent_to+infty_in x0 by A13, A4, A9, LIMFUNC2:71;
hence f ^ is_divergent_to+infty_in x0 by A12, Th12; :: thesis: verum