let f be PartFunc of REAL,REAL; :: thesis: ( f is convergent_in+infty & lim_in+infty f <> 0 & ( for r being Real ex g being Real st
( r < g & g in dom f & f . g <> 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: lim_in+infty f <> 0 and
A3: for r being Real ex g being Real st
( r < g & g in dom f & f . g <> 0 ) ; :: thesis: ( f ^ is convergent_in+infty & lim_in+infty (f ^) = (lim_in+infty f) " )

A4: 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
A5: seq is divergent_to+infty and
A6: rng seq c= dom (f ^) ; :: thesis: ( (f ^) /* seq is convergent & lim ((f ^) /* seq) = (lim_in+infty f) " )
( dom (f ^) = (dom f) \ (f " {0}) & (dom f) \ (f " {0}) c= dom f ) by RFUNCT_1:def 2, XBOOLE_1:36;
then rng seq c= dom f by A6;
then A7: ( f /* seq is convergent & lim (f /* seq) = lim_in+infty f ) by A1, A5, Def12;
then (f /* seq) " is convergent by A2, A6, RFUNCT_2:11, SEQ_2:21;
hence (f ^) /* seq is convergent by A6, RFUNCT_2:12; :: thesis: lim ((f ^) /* seq) = (lim_in+infty f) "
thus lim ((f ^) /* seq) = lim ((f /* seq) ") by A6, RFUNCT_2:12
.= (lim_in+infty f) " by A2, A6, A7, RFUNCT_2:11, SEQ_2:22 ; :: thesis: verum

end;

now :: thesis: for r being Real ex g being Real st
( r < g & g in dom (f ^) )

let r be Real; :: thesis: ex g being Real st
( r < g & g in dom (f ^) )
consider g being Real such that
A8: r < g and
A9: g in dom f and
A10: f . g <> 0 by A3;
take g = g; :: thesis: ( r < g & g in dom (f ^) )
not f . g in {0} by A10, TARSKI:def 1;
then not g in f " {0} by FUNCT_1:def 7;
then g in (dom f) \ (f " {0}) by A9, XBOOLE_0:def 5;
hence ( r < g & g in dom (f ^) ) by A8, RFUNCT_1:def 2; :: thesis: verum

end;

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