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 8 ;

A5: now

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, A3, A4, A6, A7, Def13;
then (f /* seq) " is convergent by A3, A7, RFUNCT_2:26, SEQ_2:35;
hence (f ^ ) /* seq is convergent by A7, RFUNCT_2:27; :: thesis: lim ((f ^ ) /* seq) = (lim_in-infty f) "
thus lim ((f ^ ) /* seq) = lim ((f /* seq) " ) by A7, RFUNCT_2:27
.= (lim_in-infty f) " by A3, A7, A8, RFUNCT_2:26, SEQ_2:36 ; :: thesis: verum

end;

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