let x0 be Real; :: thesis: for f1, f2 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 (f1 (#) f2) ) ) & ex r, r1 being Real st
( 0 < r & 0 < r1 & ( for g being Real st g in (dom f2) /\ ].(x0 - r),x0.[ holds
r1 <= f2 . g ) ) holds
f1 (#) f2 is_left_divergent_to+infty_in x0
let f1, f2 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 (f1 (#) f2) ) ) & ex r, r1 being Real st
( 0 < r & 0 < r1 & ( for g being Real st g in (dom f2) /\ ].(x0 - r),x0.[ holds
r1 <= f2 . g ) ) implies f1 (#) f2 is_left_divergent_to+infty_in x0 )
assume that
A1: f1 is_left_divergent_to+infty_in x0 and
A2: for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom (f1 (#) f2) ) ; :: thesis: ( for r, r1 being Real holds
( not 0 < r or not 0 < r1 or ex g being Real st
( g in (dom f2) /\ ].(x0 - r),x0.[ & not r1 <= f2 . g ) ) or f1 (#) f2 is_left_divergent_to+infty_in x0 )
given r, t being Real such that A3: 0 < r and
A4: 0 < t and
A5: for g being Real st g in (dom f2) /\ ].(x0 - r),x0.[ holds
t <= f2 . g ; :: thesis: f1 (#) f2 is_left_divergent_to+infty_in x0

now :: thesis: for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom (f1 (#) f2)) /\ (left_open_halfline x0) holds
(f1 (#) f2) /* seq is divergent_to+infty

let seq be Real_Sequence; :: thesis: ( seq is convergent & lim seq = x0 & rng seq c= (dom (f1 (#) f2)) /\ (left_open_halfline x0) implies (f1 (#) f2) /* seq is divergent_to+infty )
assume that
A6: seq is convergent and
A7: lim seq = x0 and
A8: rng seq c= (dom (f1 (#) f2)) /\ (left_open_halfline x0) ; :: thesis: (f1 (#) f2) /* seq is divergent_to+infty
x0 - r < x0 by A3, Lm1;
then consider k being Nat such that
A9: for n being Nat st k <= n holds
x0 - r < seq . n by A6, A7, Th1;
A10: rng seq c= dom (f1 (#) f2) by A8, Lm2;
A11: dom (f1 (#) f2) = (dom f1) /\ (dom f2) by A8, Lm2;
rng (seq ^\ k) c= rng seq by VALUED_0:21;
then A12: rng (seq ^\ k) c= (dom (f1 (#) f2)) /\ (left_open_halfline x0) by A8, XBOOLE_1:1;
then A13: rng (seq ^\ k) c= dom f2 by Lm2;
A14: rng (seq ^\ k) c= left_open_halfline x0 by A12, Lm2;

A15: now :: thesis: ( 0 < t & ( for n being Nat holds t <= (f2 /* (seq ^\ k)) . n ) )

thus 0 < t by A4; :: thesis: for n being Nat holds t <= (f2 /* (seq ^\ k)) . n
let n be Nat; :: thesis: t <= (f2 /* (seq ^\ k)) . n
A16: n in NAT by ORDINAL1:def 12;
x0 - r < seq . (n + k) by A9, NAT_1:12;
then A17: x0 - r < (seq ^\ k) . n by NAT_1:def 3;
A18: (seq ^\ k) . n in rng (seq ^\ k) by VALUED_0:28;
then (seq ^\ k) . n in left_open_halfline x0 by A14;
then (seq ^\ k) . n in { g1 where g1 is Real : g1 < x0 } by XXREAL_1:229;
then ex g being Real st
( g = (seq ^\ k) . n & g < x0 ) ;
then (seq ^\ k) . n in { g2 where g2 is Real : ( x0 - r < g2 & g2 < x0 ) } by A17;
then (seq ^\ k) . n in ].(x0 - r),x0.[ by RCOMP_1:def 2;
then (seq ^\ k) . n in (dom f2) /\ ].(x0 - r),x0.[ by A13, A18, XBOOLE_0:def 4;
then t <= f2 . ((seq ^\ k) . n) by A5;
hence t <= (f2 /* (seq ^\ k)) . n by A13, FUNCT_2:108, A16; :: thesis: verum

end;

A19: rng (seq ^\ k) c= (dom f1) /\ (left_open_halfline x0) by A12, Lm2;
lim (seq ^\ k) = x0 by A6, A7, SEQ_4:20;
then f1 /* (seq ^\ k) is divergent_to+infty by A1, A6, A19;
then A20: (f1 /* (seq ^\ k)) (#) (f2 /* (seq ^\ k)) is divergent_to+infty by A15, LIMFUNC1:22;
rng (seq ^\ k) c= dom (f1 (#) f2) by A12, Lm2;
then (f1 /* (seq ^\ k)) (#) (f2 /* (seq ^\ k)) = (f1 (#) f2) /* (seq ^\ k) by A11, RFUNCT_2:8
.= ((f1 (#) f2) /* seq) ^\ k by A10, VALUED_0:27 ;
hence (f1 (#) f2) /* seq is divergent_to+infty by A20, LIMFUNC1:7; :: thesis: verum

end;

hence f1 (#) f2 is_left_divergent_to+infty_in x0 by A2; :: thesis: verum