let x0 be Real; for seq being Real_Sequence
for f being PartFunc of REAL,REAL st ( for g1 being Real ex r being Real st
( x0 < r & ( for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds
f . r1 < g1 ) ) ) & seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) holds
f /* seq is divergent_to-infty
let seq be Real_Sequence; for f being PartFunc of REAL,REAL st ( for g1 being Real ex r being Real st
( x0 < r & ( for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds
f . r1 < g1 ) ) ) & seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) holds
f /* seq is divergent_to-infty
let f be PartFunc of REAL,REAL; ( ( for g1 being Real ex r being Real st
( x0 < r & ( for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds
f . r1 < g1 ) ) ) & seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) implies f /* seq is divergent_to-infty )
assume that
A1:
for g1 being Real ex r being Real st
( x0 < r & ( for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds
f . r1 < g1 ) )
and
A2:
seq is convergent
and
A3:
lim seq = x0
and
A4:
rng seq c= (dom f) /\ (right_open_halfline x0)
; f /* seq is divergent_to-infty
A5:
(dom f) /\ (right_open_halfline x0) c= dom f
by XBOOLE_1:17;
now for g1 being Real ex n being Nat st
for k being Nat st n <= k holds
(f /* seq) . k < g1let g1 be
Real;
ex n being Nat st
for k being Nat st n <= k holds
(f /* seq) . k < g1consider r being
Real such that A6:
x0 < r
and A7:
for
r1 being
Real st
r1 < r &
x0 < r1 &
r1 in dom f holds
f . r1 < g1
by A1;
consider n being
Nat such that A8:
for
k being
Nat st
n <= k holds
seq . k < r
by A2, A3, A6, Th2;
take n =
n;
for k being Nat st n <= k holds
(f /* seq) . k < g1let k be
Nat;
( n <= k implies (f /* seq) . k < g1 )assume A9:
n <= k
;
(f /* seq) . k < g1A10:
seq . k in rng seq
by VALUED_0:28;
then
seq . k in right_open_halfline x0
by A4, XBOOLE_0:def 4;
then
seq . k in { g2 where g2 is Real : x0 < g2 }
by XXREAL_1:230;
then A11:
ex
g2 being
Real st
(
g2 = seq . k &
x0 < g2 )
;
A12:
k in NAT
by ORDINAL1:def 12;
seq . k in dom f
by A4, A10, XBOOLE_0:def 4;
then
f . (seq . k) < g1
by A7, A8, A9, A11;
hence
(f /* seq) . k < g1
by A4, A5, FUNCT_2:108, XBOOLE_1:1, A12;
verum end;
hence
f /* seq is divergent_to-infty
; verum