let f, f1 be PartFunc of REAL,REAL; :: thesis: ( f1 is divergent_in+infty_to+infty & ( for r being Real ex g being Real st
( r < g & g in dom f ) ) & ex r being Real st
( (dom f) /\ (right_open_halfline r) c= (dom f1) /\ (right_open_halfline r) & ( for g being Real st g in (dom f) /\ (right_open_halfline r) holds
f1 . g <= f . g ) ) implies f is divergent_in+infty_to+infty )
assume that
A1: f1 is divergent_in+infty_to+infty and
A2: for r being Real ex g being Real st
( r < g & g in dom f ) ; :: thesis: ( for r being Real holds
( not (dom f) /\ (right_open_halfline r) c= (dom f1) /\ (right_open_halfline r) or ex g being Real st
( g in (dom f) /\ (right_open_halfline r) & not f1 . g <= f . g ) ) or f is divergent_in+infty_to+infty )
given r1 being Real such that A3: (dom f) /\ (right_open_halfline r1) c= (dom f1) /\ (right_open_halfline r1) and
A4: for g being Real st g in (dom f) /\ (right_open_halfline r1) holds
f1 . g <= f . g ; :: thesis: f is divergent_in+infty_to+infty

now :: thesis: for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds
f /* seq is divergent_to+infty

let seq be Real_Sequence; :: thesis: ( seq is divergent_to+infty & rng seq c= dom f implies f /* seq is divergent_to+infty )
assume that
A5: seq is divergent_to+infty and
A6: rng seq c= dom f ; :: thesis: f /* seq is divergent_to+infty
consider k being Nat such that
A7: for n being Nat st k <= n holds
r1 < seq . n by A5;

now :: thesis: for x being object st x in rng (seq ^\ k) holds
x in right_open_halfline r1

let x be object ; :: thesis: ( x in rng (seq ^\ k) implies x in right_open_halfline r1 )
assume x in rng (seq ^\ k) ; :: thesis: x in right_open_halfline r1
then consider n being Element of NAT such that
A8: (seq ^\ k) . n = x by FUNCT_2:113;
r1 < seq . (n + k) by A7, NAT_1:12;
then r1 < (seq ^\ k) . n by NAT_1:def 3;
then x in { g2 where g2 is Real : r1 < g2 } by A8;
hence x in right_open_halfline r1 by XXREAL_1:230; :: thesis: verum

end;

then A9: rng (seq ^\ k) c= right_open_halfline r1 ;
A10: rng (seq ^\ k) c= rng seq by VALUED_0:21;
then rng (seq ^\ k) c= dom f by A6;
then A11: rng (seq ^\ k) c= (dom f) /\ (right_open_halfline r1) by A9, XBOOLE_1:19;
then A12: rng (seq ^\ k) c= (dom f1) /\ (right_open_halfline r1) by A3;
A13: (dom f1) /\ (right_open_halfline r1) c= dom f1 by XBOOLE_1:17;

A14: 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
A15: 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 A4, A11;
then (f1 /* (seq ^\ k)) . n <= f . ((seq ^\ k) . n) by A12, A13, FUNCT_2:108, XBOOLE_1:1, A15;
hence (f1 /* (seq ^\ k)) . n <= (f /* (seq ^\ k)) . n by A6, A10, FUNCT_2:108, XBOOLE_1:1, A15; :: thesis: verum

end;

A16: seq ^\ k is divergent_to+infty by A5, Th26;
rng (seq ^\ k) c= dom f1 by A12, A13;
then f1 /* (seq ^\ k) is divergent_to+infty by A1, A16;
then A17: f /* (seq ^\ k) is divergent_to+infty by A14, Th42;
f /* (seq ^\ k) = (f /* seq) ^\ k by A6, VALUED_0:27;
hence f /* seq is divergent_to+infty by A17, Th7; :: thesis: verum

end;

hence f is divergent_in+infty_to+infty by A2; :: thesis: verum