let f be PartFunc of REAL,REAL; :: thesis: ( 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 ; :: thesis: ( 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 :: thesis: 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; :: thesis: ( 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 ^) ; :: thesis: ( (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, Def12;
then (f /* seq) " is convergent by A3, A7, RFUNCT_2:11, SEQ_2:21;
hence (f ^) /* seq is convergent by A7, RFUNCT_2:12; :: thesis: 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 ; :: thesis: verum

end;

for r being Real ex g being Real st
( r < g & g in dom (f ^) ) by A1, A4;
hence f ^ is convergent_in+infty by A5; :: thesis: lim_in+infty (f ^) = (lim_in+infty f) "
hence lim_in+infty (f ^) = (lim_in+infty f) " by A5, Def12; :: thesis: verum