let f be PartFunc of REAL,REAL; ( f is convergent_in+infty & lim_in+infty f <> 0 & ( for r being Real ex g being Real st
( r < g & g in dom f & f . g <> 0 ) ) implies ( f ^ is convergent_in+infty & lim_in+infty (f ^) = (lim_in+infty f) " ) )
assume that
A1:
f is convergent_in+infty
and
A2:
lim_in+infty f <> 0
and
A3:
for r being Real ex g being Real st
( r < g & g in dom f & f . g <> 0 )
; ( f ^ is convergent_in+infty & lim_in+infty (f ^) = (lim_in+infty f) " )
A4:
now for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom (f ^) holds
( (f ^) /* seq is convergent & lim ((f ^) /* seq) = (lim_in+infty f) " )let seq be
Real_Sequence;
( seq is divergent_to+infty & rng seq c= dom (f ^) implies ( (f ^) /* seq is convergent & lim ((f ^) /* seq) = (lim_in+infty f) " ) )assume that A5:
seq is
divergent_to+infty
and A6:
rng seq c= dom (f ^)
;
( (f ^) /* seq is convergent & lim ((f ^) /* seq) = (lim_in+infty f) " )
(
dom (f ^) = (dom f) \ (f " {0}) &
(dom f) \ (f " {0}) c= dom f )
by RFUNCT_1:def 2, XBOOLE_1:36;
then
rng seq c= dom f
by A6;
then A7:
(
f /* seq is
convergent &
lim (f /* seq) = lim_in+infty f )
by A1, A5, Def12;
then
(f /* seq) " is
convergent
by A2, A6, RFUNCT_2:11, SEQ_2:21;
hence
(f ^) /* seq is
convergent
by A6, RFUNCT_2:12;
lim ((f ^) /* seq) = (lim_in+infty f) " thus lim ((f ^) /* seq) =
lim ((f /* seq) ")
by A6, RFUNCT_2:12
.=
(lim_in+infty f) "
by A2, A6, A7, RFUNCT_2:11, SEQ_2:22
;
verum end;
hence
f ^ is convergent_in+infty
by A4; lim_in+infty (f ^) = (lim_in+infty f) "
hence
lim_in+infty (f ^) = (lim_in+infty f) "
by A4, Def12; verum