let f1, f2 be PartFunc of REAL ,REAL ; :: thesis: ( f1 is convergent_in-infty & f2 is_convergent_in lim_in-infty f1 & ( for r being Real ex g being Real st
( g < r & g in dom (f2 * f1) ) ) & ex r being Real st
for g being Real st g in (dom f1) /\ (left_open_halfline r) holds
f1 . g <> lim_in-infty f1 implies ( f2 * f1 is convergent_in-infty & lim_in-infty (f2 * f1) = lim f2,(lim_in-infty f1) ) )
assume A1:
( f1 is convergent_in-infty & f2 is_convergent_in lim_in-infty f1 & ( for r being Real ex g being Real st
( g < r & g in dom (f2 * f1) ) ) )
; :: thesis: ( for r being Real ex g being Real st
( g in (dom f1) /\ (left_open_halfline r) & not f1 . g <> lim_in-infty f1 ) or ( f2 * f1 is convergent_in-infty & lim_in-infty (f2 * f1) = lim f2,(lim_in-infty f1) ) )
given r being Real such that A2:
for g being Real st g in (dom f1) /\ (left_open_halfline r) holds
f1 . g <> lim_in-infty f1
; :: thesis: ( f2 * f1 is convergent_in-infty & lim_in-infty (f2 * f1) = lim f2,(lim_in-infty f1) )
A3:
now let s be
Real_Sequence;
:: thesis: ( s is divergent_to-infty & rng s c= dom (f2 * f1) implies ( (f2 * f1) /* s is convergent & lim ((f2 * f1) /* s) = lim f2,(lim_in-infty f1) ) )assume A4:
(
s is
divergent_to-infty &
rng s c= dom (f2 * f1) )
;
:: thesis: ( (f2 * f1) /* s is convergent & lim ((f2 * f1) /* s) = lim f2,(lim_in-infty f1) )then consider k being
Element of
NAT such that A5:
for
n being
Element of
NAT st
k <= n holds
s . n < r
by LIMFUNC1:def 5;
set q =
s ^\ k;
A6:
s ^\ k is
divergent_to-infty
by A4, LIMFUNC1:54;
A7:
(
rng s c= dom f1 &
rng (f1 /* s) c= dom f2 )
by A4, Lm2;
A8:
rng (s ^\ k) c= rng s
by VALUED_0:21;
then
rng (s ^\ k) c= dom f1
by A7, XBOOLE_1:1;
then A9:
(
f1 /* (s ^\ k) is
convergent &
lim (f1 /* (s ^\ k)) = lim_in-infty f1 )
by A1, A6, LIMFUNC1:def 13;
set L =
lim f2,
(lim_in-infty f1);
A10:
lim f2,
(lim_in-infty f1) = lim f2,
(lim_in-infty f1)
;
rng (f1 /* (s ^\ k)) c= (dom f2) \ {(lim_in-infty f1)}
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in rng (f1 /* (s ^\ k)) or x in (dom f2) \ {(lim_in-infty f1)} )
assume
x in rng (f1 /* (s ^\ k))
;
:: thesis: x in (dom f2) \ {(lim_in-infty f1)}
then consider n being
Element of
NAT such that A11:
(f1 /* (s ^\ k)) . n = x
by FUNCT_2:190;
A12:
x =
f1 . ((s ^\ k) . n)
by A7, A8, A11, FUNCT_2:185, XBOOLE_1:1
.=
f1 . (s . (n + k))
by NAT_1:def 3
;
(f1 /* s) . (n + k) in rng (f1 /* s)
by VALUED_0:28;
then
(f1 /* s) . (n + k) in dom f2
by A7;
then A13:
x in dom f2
by A7, A12, FUNCT_2:185;
s . (n + k) < r
by A5, NAT_1:12;
then
s . (n + k) in { r2 where r2 is Real : r2 < r }
;
then A14:
s . (n + k) in left_open_halfline r
by XXREAL_1:229;
s . (n + k) in rng s
by VALUED_0:28;
then
s . (n + k) in (dom f1) /\ (left_open_halfline r)
by A7, A14, XBOOLE_0:def 4;
then
f1 . (s . (n + k)) <> lim_in-infty f1
by A2;
then
not
f1 . (s . (n + k)) in {(lim_in-infty f1)}
by TARSKI:def 1;
hence
x in (dom f2) \ {(lim_in-infty f1)}
by A12, A13, XBOOLE_0:def 5;
:: thesis: verum
end; then A15:
(
f2 /* (f1 /* (s ^\ k)) is
convergent &
lim (f2 /* (f1 /* (s ^\ k))) = lim f2,
(lim_in-infty f1) )
by A1, A9, A10, LIMFUNC3:def 4;
A16:
f2 /* (f1 /* (s ^\ k)) =
f2 /* ((f1 /* s) ^\ k)
by A7, VALUED_0:27
.=
(f2 /* (f1 /* s)) ^\ k
by A7, VALUED_0:27
.=
((f2 * f1) /* s) ^\ k
by A4, VALUED_0:31
;
hence
(f2 * f1) /* s is
convergent
by A15, SEQ_4:35;
:: thesis: lim ((f2 * f1) /* s) = lim f2,(lim_in-infty f1)thus
lim ((f2 * f1) /* s) = lim f2,
(lim_in-infty f1)
by A15, A16, SEQ_4:36;
:: thesis: verum end;
hence
f2 * f1 is convergent_in-infty
by A1, LIMFUNC1:def 9; :: thesis: lim_in-infty (f2 * f1) = lim f2,(lim_in-infty f1)
hence
lim_in-infty (f2 * f1) = lim f2,(lim_in-infty f1)
by A3, LIMFUNC1:def 13; :: thesis: verum