let x0 be Real; :: thesis: 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; :: thesis: 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; :: thesis: ( ( 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) ; :: thesis: f /* seq is divergent_to-infty
A5: (dom f) /\ (right_open_halfline x0) c= dom f by XBOOLE_1:17;

now

let g1 be Real; :: thesis: ex n being Element of NAT st
for k being Element of NAT st n <= k holds
(f /* seq) . k < g1
consider 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 Element of NAT such that
A8: for k being Element of NAT st n <= k holds
seq . k < r by A2, A3, A6, Th2;
take n = n; :: thesis: for k being Element of NAT st n <= k holds
(f /* seq) . k < g1
let k be Element of NAT ; :: thesis: ( n <= k implies (f /* seq) . k < g1 )
assume A9: n <= k ; :: thesis: (f /* seq) . k < g1
A10: 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 ) ;
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; :: thesis: verum

end;

hence f /* seq is divergent_to-infty by LIMFUNC1:def 5; :: thesis: verum