let f be PartFunc of REAL , REAL ; :: thesis: ( f is convergent_in+infty implies ( abs f is convergent_in+infty & lim_in+infty (abs f) = abs (lim_in+infty f) ) )
assume A1: f is convergent_in+infty ; :: thesis: ( abs f is convergent_in+infty & lim_in+infty (abs f) = abs (lim_in+infty f) )

A2: now

let r be Real; :: thesis: ex g being Real st
( r < g & g in dom (abs f) )
consider g being Real such that
A3: ( r < g & g in dom f ) by A1, Def6;
take g = g; :: thesis: ( r < g & g in dom (abs f) )
thus ( r < g & g in dom (abs f) ) by A3, VALUED_1:def 11; :: thesis: verum

end;

A4: now

let seq be Real_Sequence; :: thesis: ( seq is divergent_to+infty & rng seq c= dom (abs f) implies ( (abs f) /* seq is convergent & lim ((abs f) /* seq) = abs (lim_in+infty f) ) )
A5: lim_in+infty f = lim_in+infty f ;
assume ( seq is divergent_to+infty & rng seq c= dom (abs f) ) ; :: thesis: ( (abs f) /* seq is convergent & lim ((abs f) /* seq) = abs (lim_in+infty f) )
then A6: ( seq is divergent_to+infty & rng seq c= dom f ) by VALUED_1:def 11;
then A7: ( f /* seq is convergent & lim (f /* seq) = lim_in+infty f ) by A1, A5, Def12;
then abs (f /* seq) is convergent by SEQ_4:26;
hence (abs f) /* seq is convergent by A6, RFUNCT_2:25; :: thesis: lim ((abs f) /* seq) = abs (lim_in+infty f)
thus lim ((abs f) /* seq) = lim (abs (f /* seq)) by A6, RFUNCT_2:25
.= abs (lim_in+infty f) by A7, SEQ_4:27 ; :: thesis: verum

end;

hence abs f is convergent_in+infty by A2, Def6; :: thesis: lim_in+infty (abs f) = abs (lim_in+infty f)
hence lim_in+infty (abs f) = abs (lim_in+infty f) by A4, Def12; :: thesis: verum