let x0 be Real; 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; ( 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) )
; ( 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
; f1 (#) f2 is_left_divergent_to+infty_in x0
now 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;
( 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)
;
(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 ( 0 < t & ( for n being Nat holds t <= (f2 /* (seq ^\ k)) . n ) )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;
verum end;
hence
f1 (#) f2 is_left_divergent_to+infty_in x0
by A2; verum