let f be PartFunc of REAL,REAL; for x0 being Real st f is_right_divergent_to-infty_in x0 holds
ex r being Real st
( 0 < r & f | ].x0,(x0 + r).[ is bounded_above )
let x0 be Real; ( f is_right_divergent_to-infty_in x0 implies ex r being Real st
( 0 < r & f | ].x0,(x0 + r).[ is bounded_above ) )
assume A1:
f is_right_divergent_to-infty_in x0
; ex r being Real st
( 0 < r & f | ].x0,(x0 + r).[ is bounded_above )
consider r being Real such that
A2:
x0 < r
and
A3:
for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds
f . r1 < 1
by A1, LIMFUNC2:12;
set R = r - x0;
for r1 being object st r1 in dom (f | ].x0,(x0 + (r - x0)).[) holds
(f | ].x0,(x0 + (r - x0)).[) . r1 < 1
proof
let r1 be
object ;
( r1 in dom (f | ].x0,(x0 + (r - x0)).[) implies (f | ].x0,(x0 + (r - x0)).[) . r1 < 1 )
assume A4:
r1 in dom (f | ].x0,(x0 + (r - x0)).[)
;
(f | ].x0,(x0 + (r - x0)).[) . r1 < 1
then reconsider r1 =
r1 as
Real ;
r1 in (dom f) /\ ].x0,(x0 + (r - x0)).[
by A4, RELAT_1:61;
then A5:
(
r1 in dom f &
r1 in ].x0,(x0 + (r - x0)).[ )
by XBOOLE_0:def 4;
then
(
x0 < r1 &
r1 < x0 + (r - x0) )
by XXREAL_1:4;
then
f . r1 < 1
by A3, A5;
hence
(f | ].x0,(x0 + (r - x0)).[) . r1 < 1
by A5, FUNCT_1:49;
verum
end;
then
f | ].x0,(x0 + (r - x0)).[ is bounded_above
by SEQ_2:def 1;
hence
ex r being Real st
( 0 < r & f | ].x0,(x0 + r).[ is bounded_above )
by A2, XREAL_1:50; verum