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, Def12;
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
( r < g & g in dom (f ^ ) ) by A1, A4, Def6;
hence f ^ is convergent_in+infty by A5, Def6; :: thesis: lim_in+infty (f ^ ) = (lim_in+infty f) "
hence lim_in+infty (f ^ ) = (lim_in+infty f) " by A5, Def12; :: thesis: verum