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

now

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

end;

then rng (seq ^\ k) c= ].(x0 - r),x0.[ by TARSKI:def 3;
then A13: rng (seq ^\ k) c= (dom f) /\ ].(x0 - r),x0.[ by A9, XBOOLE_1:19;
then A14: rng (seq ^\ k) c= (dom f1) /\ ].(x0 - r),x0.[ by A2, XBOOLE_1:1;
A15: (dom f1) /\ ].(x0 - r),x0.[ c= dom f1 by XBOOLE_1:17;
then rng (seq ^\ k) c= dom f1 by A14, XBOOLE_1:1;
then rng (seq ^\ k) c= (dom f1) /\ (left_open_halfline x0) by A9, XBOOLE_1:19;
then A16: f1 /* (seq ^\ k) is divergent_to-infty by A1, A5, Def3;

now

let n be Element of NAT ; :: thesis: (f /* (seq ^\ k)) . n <= (f1 /* (seq ^\ k)) . n
(seq ^\ k) . n in rng (seq ^\ k) by VALUED_0:28;
then f . ((seq ^\ k) . n) <= f1 . ((seq ^\ k) . n) by A2, A13;
then (f /* (seq ^\ k)) . n <= f1 . ((seq ^\ k) . n) by A7, A8, FUNCT_2:185, XBOOLE_1:1;
hence (f /* (seq ^\ k)) . n <= (f1 /* (seq ^\ k)) . n by A14, A15, FUNCT_2:185, XBOOLE_1:1; :: thesis: verum

end;

then f /* (seq ^\ k) is divergent_to-infty by A16, LIMFUNC1:70;
then (f /* seq) ^\ k is divergent_to-infty by A3, A6, VALUED_0:27, XBOOLE_1:1;
hence f /* seq is divergent_to-infty by LIMFUNC1:34; :: thesis: verum