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 A1: ( f is convergent_in+infty & f " {0 } = {} & lim_in+infty f <> 0 ) ; :: thesis: ( f ^ is convergent_in+infty & lim_in+infty (f ^ ) = (lim_in+infty f) " )
then A2: dom f = (dom f) \ (f " {0 })
.= dom (f ^ ) by RFUNCT_1:def 8 ;
then A3: for r being Real ex g being Real st
( r < g & g in dom (f ^ ) ) by A1, Def6;

A4: 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 A5: ( seq is divergent_to+infty & rng seq c= dom (f ^ ) ) ; :: thesis: ( (f ^ ) /* seq is convergent & lim ((f ^ ) /* seq) = (lim_in+infty f) " )
then A6: ( f /* seq is convergent & lim (f /* seq) = lim_in+infty f ) by A1, A2, Def12;
then (f /* seq) " is convergent by A1, A5, RFUNCT_2:26, SEQ_2:35;
hence (f ^ ) /* seq is convergent by A5, RFUNCT_2:27; :: thesis: lim ((f ^ ) /* seq) = (lim_in+infty f) "
thus lim ((f ^ ) /* seq) = lim ((f /* seq) " ) by A5, RFUNCT_2:27
.= (lim_in+infty f) " by A1, A5, A6, RFUNCT_2:26, SEQ_2:36 ; :: thesis: verum

end;

hence f ^ is convergent_in+infty by A3, Def6; :: thesis: lim_in+infty (f ^ ) = (lim_in+infty f) "
hence lim_in+infty (f ^ ) = (lim_in+infty f) " by A4, Def12; :: thesis: verum