let x0 be Real; :: thesis: for f, f1 being PartFunc of REAL,REAL st f1 is_divergent_to-infty_in x0 & ex r being Real st
( 0 < r & ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ c= (dom f) /\ (dom f1) & ( for g being Real st g in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ holds
f . g <= f1 . g ) ) holds
f is_divergent_to-infty_in x0
let f, f1 be PartFunc of REAL,REAL; :: thesis: ( f1 is_divergent_to-infty_in x0 & ex r being Real st
( 0 < r & ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ c= (dom f) /\ (dom f1) & ( for g being Real st g in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ holds
f . g <= f1 . g ) ) implies f is_divergent_to-infty_in x0 )
assume A1: f1 is_divergent_to-infty_in x0 ; :: thesis: ( for r being Real holds
( not 0 < r or not ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ c= (dom f) /\ (dom f1) or ex g being Real st
( g in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ & not f . g <= f1 . g ) ) or f is_divergent_to-infty_in x0 )
given r being Real such that A2: 0 < r and
A3: ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ c= (dom f) /\ (dom f1) and
A4: for g being Real st g in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ holds
f . g <= f1 . g ; :: thesis: f is_divergent_to-infty_in x0
A5: ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ = (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) by A3, XBOOLE_1:18, XBOOLE_1:28;
A6: ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ = (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) by A3, XBOOLE_1:18, XBOOLE_1:28;
for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) by A2, A3, Th5, XBOOLE_1:18;
hence f is_divergent_to-infty_in x0 by A1, A2, A4, A5, A6, Th25; :: thesis: verum