let f1, f2 be PartFunc of REAL,REAL; ( f1 is convergent_in+infty & f2 is_right_convergent_in lim_in+infty f1 & ( for r being Real ex g being Real st
( r < g & g in dom (f2 * f1) ) ) & ex r being Real st
for g being Real st g in (dom f1) /\ (right_open_halfline r) holds
lim_in+infty f1 < f1 . g implies ( f2 * f1 is convergent_in+infty & lim_in+infty (f2 * f1) = lim_right (f2,(lim_in+infty f1)) ) )
assume that
A1:
f1 is convergent_in+infty
and
A2:
f2 is_right_convergent_in lim_in+infty f1
and
A3:
for r being Real ex g being Real st
( r < g & g in dom (f2 * f1) )
; ( for r being Real ex g being Real st
( g in (dom f1) /\ (right_open_halfline r) & not lim_in+infty f1 < f1 . g ) or ( f2 * f1 is convergent_in+infty & lim_in+infty (f2 * f1) = lim_right (f2,(lim_in+infty f1)) ) )
given r being Real such that A4:
for g being Real st g in (dom f1) /\ (right_open_halfline r) holds
lim_in+infty f1 < f1 . g
; ( f2 * f1 is convergent_in+infty & lim_in+infty (f2 * f1) = lim_right (f2,(lim_in+infty f1)) )
A5:
now for s being Real_Sequence st s is divergent_to+infty & rng s c= dom (f2 * f1) holds
( (f2 * f1) /* s is convergent & lim ((f2 * f1) /* s) = lim_right (f2,(lim_in+infty f1)) )set L =
lim_right (
f2,
(lim_in+infty f1));
let s be
Real_Sequence;
( s is divergent_to+infty & rng s c= dom (f2 * f1) implies ( (f2 * f1) /* s is convergent & lim ((f2 * f1) /* s) = lim_right (f2,(lim_in+infty f1)) ) )assume that A6:
s is
divergent_to+infty
and A7:
rng s c= dom (f2 * f1)
;
( (f2 * f1) /* s is convergent & lim ((f2 * f1) /* s) = lim_right (f2,(lim_in+infty f1)) )consider k being
Nat such that A8:
for
n being
Nat st
k <= n holds
r < s . n
by A6;
set q =
s ^\ k;
A9:
s ^\ k is
divergent_to+infty
by A6, LIMFUNC1:26;
A10:
rng s c= dom f1
by A7, Lm2;
A11:
rng (s ^\ k) c= rng s
by VALUED_0:21;
then
rng (s ^\ k) c= dom f1
by A10;
then A12:
(
f1 /* (s ^\ k) is
convergent &
lim (f1 /* (s ^\ k)) = lim_in+infty f1 )
by A1, A9, LIMFUNC1:def 12;
A13:
rng (f1 /* s) c= dom f2
by A7, Lm2;
A14:
rng (f1 /* (s ^\ k)) c= (dom f2) /\ (right_open_halfline (lim_in+infty f1))
proof
let x be
object ;
TARSKI:def 3 ( not x in rng (f1 /* (s ^\ k)) or x in (dom f2) /\ (right_open_halfline (lim_in+infty f1)) )
assume
x in rng (f1 /* (s ^\ k))
;
x in (dom f2) /\ (right_open_halfline (lim_in+infty f1))
then consider n being
Element of
NAT such that A15:
(f1 /* (s ^\ k)) . n = x
by FUNCT_2:113;
A16:
x =
f1 . ((s ^\ k) . n)
by A10, A11, A15, FUNCT_2:108, XBOOLE_1:1
.=
f1 . (s . (n + k))
by NAT_1:def 3
;
r < s . (n + k)
by A8, NAT_1:12;
then
s . (n + k) in { r2 where r2 is Real : r < r2 }
;
then A17:
s . (n + k) in right_open_halfline r
by XXREAL_1:230;
s . (n + k) in rng s
by VALUED_0:28;
then
s . (n + k) in (dom f1) /\ (right_open_halfline r)
by A10, A17, XBOOLE_0:def 4;
then
lim_in+infty f1 < f1 . (s . (n + k))
by A4;
then
x in { g1 where g1 is Real : lim_in+infty f1 < g1 }
by A16;
then A18:
x in right_open_halfline (lim_in+infty f1)
by XXREAL_1:230;
A19:
n + k in NAT
by ORDINAL1:def 12;
(f1 /* s) . (n + k) in rng (f1 /* s)
by VALUED_0:28;
then
(f1 /* s) . (n + k) in dom f2
by A13;
then
x in dom f2
by A10, A16, FUNCT_2:108, A19;
hence
x in (dom f2) /\ (right_open_halfline (lim_in+infty f1))
by A18, XBOOLE_0:def 4;
verum
end; A20:
f2 /* (f1 /* (s ^\ k)) =
f2 /* ((f1 /* s) ^\ k)
by A10, VALUED_0:27
.=
(f2 /* (f1 /* s)) ^\ k
by A13, VALUED_0:27
.=
((f2 * f1) /* s) ^\ k
by A7, VALUED_0:31
;
lim_right (
f2,
(lim_in+infty f1))
= lim_right (
f2,
(lim_in+infty f1))
;
then A21:
f2 /* (f1 /* (s ^\ k)) is
convergent
by A2, A12, A14, LIMFUNC2:def 8;
hence
(f2 * f1) /* s is
convergent
by A20, SEQ_4:21;
lim ((f2 * f1) /* s) = lim_right (f2,(lim_in+infty f1))
lim (f2 /* (f1 /* (s ^\ k))) = lim_right (
f2,
(lim_in+infty f1))
by A2, A12, A14, LIMFUNC2:def 8;
hence
lim ((f2 * f1) /* s) = lim_right (
f2,
(lim_in+infty f1))
by A21, A20, SEQ_4:22;
verum end;
hence
f2 * f1 is convergent_in+infty
by A3; lim_in+infty (f2 * f1) = lim_right (f2,(lim_in+infty f1))
hence
lim_in+infty (f2 * f1) = lim_right (f2,(lim_in+infty f1))
by A5, LIMFUNC1:def 12; verum