let f be PartFunc of REAL,REAL; ( f is convergent_in-infty & f " {0} = {} & lim_in-infty f <> 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:
f " {0} = {}
and
A3:
lim_in-infty f <> 0
; ( f ^ is convergent_in-infty & lim_in-infty (f ^) = (lim_in-infty f) " )
A4: dom f =
(dom f) \ (f " {0})
by A2
.=
dom (f ^)
by RFUNCT_1:def 2
;
A5:
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 A6:
seq is
divergent_to-infty
and A7:
rng seq c= dom (f ^)
;
( (f ^) /* seq is convergent & lim ((f ^) /* seq) = (lim_in-infty f) " )A8:
(
f /* seq is
convergent &
lim (f /* seq) = lim_in-infty f )
by A1, A4, A6, A7, Def13;
then
(f /* seq) " is
convergent
by A3, A7, RFUNCT_2:11, SEQ_2:21;
hence
(f ^) /* seq is
convergent
by A7, RFUNCT_2:12;
lim ((f ^) /* seq) = (lim_in-infty f) " thus lim ((f ^) /* seq) =
lim ((f /* seq) ")
by A7, RFUNCT_2:12
.=
(lim_in-infty f) "
by A3, A7, A8, RFUNCT_2:11, SEQ_2:22
;
verum end;
for r being Real ex g being Real st
( g < r & g in dom (f ^) )
by A1, A4;
hence
f ^ is convergent_in-infty
by A5; lim_in-infty (f ^) = (lim_in-infty f) "
hence
lim_in-infty (f ^) = (lim_in-infty f) "
by A5, Def13; verum