let f1, f2 be PartFunc of REAL,REAL; ( f1 is convergent_in-infty & lim_in-infty f1 = 0 & ( for r being Real ex g being Real st
( g < r & g in dom (f1 (#) f2) ) ) & ex r being Real st f2 | (left_open_halfline r) is bounded implies ( f1 (#) f2 is convergent_in-infty & lim_in-infty (f1 (#) f2) = 0 ) )
assume that
A1:
( f1 is convergent_in-infty & lim_in-infty f1 = 0 )
and
A2:
for r being Real ex g being Real st
( g < r & g in dom (f1 (#) f2) )
; ( for r being Real holds not f2 | (left_open_halfline r) is bounded or ( f1 (#) f2 is convergent_in-infty & lim_in-infty (f1 (#) f2) = 0 ) )
given r being Real such that A3:
f2 | (left_open_halfline r) is bounded
; ( f1 (#) f2 is convergent_in-infty & lim_in-infty (f1 (#) f2) = 0 )
consider g being Real such that
A4:
for r1 being object st r1 in (left_open_halfline r) /\ (dom f2) holds
|.(f2 . r1).| <= g
by A3, RFUNCT_1:73;
A5:
now for s being Real_Sequence st s is divergent_to-infty & rng s c= dom (f1 (#) f2) holds
( (f1 (#) f2) /* s is convergent & lim ((f1 (#) f2) /* s) = 0 )let s be
Real_Sequence;
( s is divergent_to-infty & rng s c= dom (f1 (#) f2) implies ( (f1 (#) f2) /* s is convergent & lim ((f1 (#) f2) /* s) = 0 ) )assume that A6:
s is
divergent_to-infty
and A7:
rng s c= dom (f1 (#) f2)
;
( (f1 (#) f2) /* s is convergent & lim ((f1 (#) f2) /* s) = 0 )consider k being
Nat such that A8:
for
n being
Nat st
k <= n holds
s . n < r
by A6;
A9:
rng (s ^\ k) c= rng s
by VALUED_0:21;
A10:
rng s c= dom f2
by A7, Lm3;
then A11:
rng (s ^\ k) c= dom f2
by A9;
then A14:
f2 /* (s ^\ k) is
bounded
by SEQ_2:3;
dom (f1 (#) f2) = (dom f1) /\ (dom f2)
by A7, Lm3;
then
rng (s ^\ k) c= (dom f1) /\ (dom f2)
by A7, A9;
then A15:
(f1 /* (s ^\ k)) (#) (f2 /* (s ^\ k)) =
(f1 (#) f2) /* (s ^\ k)
by RFUNCT_2:8
.=
((f1 (#) f2) /* s) ^\ k
by A7, VALUED_0:27
;
rng s c= dom f1
by A7, Lm3;
then A16:
rng (s ^\ k) c= dom f1
by A9;
s ^\ k is
divergent_to-infty
by A6, Th27;
then A17:
(
f1 /* (s ^\ k) is
convergent &
lim (f1 /* (s ^\ k)) = 0 )
by A1, A16, Def13;
then A18:
(f1 /* (s ^\ k)) (#) (f2 /* (s ^\ k)) is
convergent
by A14, SEQ_2:25;
hence
(f1 (#) f2) /* s is
convergent
by A15, SEQ_4:21;
lim ((f1 (#) f2) /* s) = 0
lim ((f1 /* (s ^\ k)) (#) (f2 /* (s ^\ k))) = 0
by A17, A14, SEQ_2:26;
hence
lim ((f1 (#) f2) /* s) = 0
by A18, A15, SEQ_4:22;
verum end;
hence
f1 (#) f2 is convergent_in-infty
by A2; lim_in-infty (f1 (#) f2) = 0
hence
lim_in-infty (f1 (#) f2) = 0
by A5, Def13; verum