let x0 be Real; :: thesis: for f, f1 being PartFunc of REAL,REAL st f1 is_right_divergent_to+infty_in x0 & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f ) ) & ex r being Real st
( 0 < r & (dom f) /\ ].x0,(x0 + r).[ c= (dom f1) /\ ].x0,(x0 + r).[ & ( for g being Real st g in (dom f) /\ ].x0,(x0 + r).[ holds
f1 . g <= f . g ) ) holds
f is_right_divergent_to+infty_in x0
let f, f1 be PartFunc of REAL,REAL; :: thesis: ( f1 is_right_divergent_to+infty_in x0 & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f ) ) & ex r being Real st
( 0 < r & (dom f) /\ ].x0,(x0 + r).[ c= (dom f1) /\ ].x0,(x0 + r).[ & ( for g being Real st g in (dom f) /\ ].x0,(x0 + r).[ holds
f1 . g <= f . g ) ) implies f is_right_divergent_to+infty_in x0 )
assume that
A1: f1 is_right_divergent_to+infty_in x0 and
A2: for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f ) ; :: thesis: ( for r being Real holds
( not 0 < r or not (dom f) /\ ].x0,(x0 + r).[ c= (dom f1) /\ ].x0,(x0 + r).[ or ex g being Real st
( g in (dom f) /\ ].x0,(x0 + r).[ & not f1 . g <= f . g ) ) or f is_right_divergent_to+infty_in x0 )
given r being Real such that A3: 0 < r and
A4: (dom f) /\ ].x0,(x0 + r).[ c= (dom f1) /\ ].x0,(x0 + r).[ and
A5: for g being Real st g in (dom f) /\ ].x0,(x0 + r).[ holds
f1 . g <= f . g ; :: thesis: f is_right_divergent_to+infty_in x0
thus for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f ) by A2; :: according to LIMFUNC2:def 5 :: thesis: for seq being Real_Sequence st 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: ( seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) implies f /* seq is divergent_to+infty )
assume that
A6: seq is convergent and
A7: lim seq = x0 and
A8: rng seq c= (dom f) /\ (right_open_halfline x0) ; :: thesis: f /* seq is divergent_to+infty
x0 < x0 + r by A3, Lm1;
then consider k being Nat such that
A9: for n being Nat st k <= n holds
seq . n < x0 + r by A6, A7, Th2;
A10: rng (seq ^\ k) c= rng seq by VALUED_0:21;
(dom f) /\ (right_open_halfline x0) c= right_open_halfline x0 by XBOOLE_1:17;
then rng seq c= right_open_halfline x0 by A8, XBOOLE_1:1;
then A11: rng (seq ^\ k) c= right_open_halfline x0 by A10, XBOOLE_1:1;

now :: thesis: for x being object st x in rng (seq ^\ k) holds
x in ].x0,(x0 + r).[

let x be object ; :: thesis: ( x in rng (seq ^\ k) implies x in ].x0,(x0 + r).[ )
assume A12: x in rng (seq ^\ k) ; :: thesis: x in ].x0,(x0 + r).[
then consider n being Element of NAT such that
A13: (seq ^\ k) . n = x by FUNCT_2:113;
(seq ^\ k) . n in right_open_halfline x0 by A11, A12, A13;
then (seq ^\ k) . n in { g where g is Real : x0 < g } by XXREAL_1:230;
then A14: ex r1 being Real st
( r1 = (seq ^\ k) . n & x0 < r1 ) ;
seq . (n + k) < x0 + r by A9, NAT_1:12;
then (seq ^\ k) . n < x0 + r by NAT_1:def 3;
then x in { g1 where g1 is Real : ( x0 < g1 & g1 < x0 + r ) } by A13, A14;
hence x in ].x0,(x0 + r).[ by RCOMP_1:def 2; :: thesis: verum

end;

then A15: rng (seq ^\ k) c= ].x0,(x0 + r).[ by TARSKI:def 3;
A16: (dom f) /\ (right_open_halfline x0) c= dom f by XBOOLE_1:17;
then A17: rng seq c= dom f by A8, XBOOLE_1:1;
then rng (seq ^\ k) c= dom f by A10, XBOOLE_1:1;
then A18: rng (seq ^\ k) c= (dom f) /\ ].x0,(x0 + r).[ by A15, XBOOLE_1:19;
then A19: rng (seq ^\ k) c= (dom f1) /\ ].x0,(x0 + r).[ by A4, XBOOLE_1:1;
A20: (dom f1) /\ ].x0,(x0 + r).[ c= dom f1 by XBOOLE_1:17;
then rng (seq ^\ k) c= dom f1 by A19, XBOOLE_1:1;
then A21: rng (seq ^\ k) c= (dom f1) /\ (right_open_halfline x0) by A11, XBOOLE_1:19;

A22: now :: thesis: for n being Nat holds (f1 /* (seq ^\ k)) . n <= (f /* (seq ^\ k)) . n

let n be Nat; :: thesis: (f1 /* (seq ^\ k)) . n <= (f /* (seq ^\ k)) . n
A23: n in NAT by ORDINAL1:def 12;
(seq ^\ k) . n in rng (seq ^\ k) by VALUED_0:28;
then f1 . ((seq ^\ k) . n) <= f . ((seq ^\ k) . n) by A5, A18;
then (f1 /* (seq ^\ k)) . n <= f . ((seq ^\ k) . n) by A19, A20, FUNCT_2:108, XBOOLE_1:1, A23;
hence (f1 /* (seq ^\ k)) . n <= (f /* (seq ^\ k)) . n by A17, A10, FUNCT_2:108, XBOOLE_1:1, A23; :: thesis: verum

end;

lim (seq ^\ k) = x0 by A6, A7, SEQ_4:20;
then f1 /* (seq ^\ k) is divergent_to+infty by A1, A6, A21;
then f /* (seq ^\ k) is divergent_to+infty by A22, LIMFUNC1:42;
then (f /* seq) ^\ k is divergent_to+infty by A8, A16, VALUED_0:27, XBOOLE_1:1;
hence f /* seq is divergent_to+infty by LIMFUNC1:7; :: thesis: verum