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) = |.(lim_in+infty f).| ) )
assume A1: f is convergent_in+infty ; :: thesis: ( abs f is convergent_in+infty & lim_in+infty (abs f) = |.(lim_in+infty f).| )

A2: now :: thesis: for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom (abs f) holds
( (abs f) /* seq is convergent & lim ((abs f) /* seq) = |.(lim_in+infty f).| )

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) = |.(lim_in+infty f).| ) )
assume that
A3: seq is divergent_to+infty and
A4: rng seq c= dom (abs f) ; :: thesis: ( (abs f) /* seq is convergent & lim ((abs f) /* seq) = |.(lim_in+infty f).| )
A5: rng seq c= dom f by A4, VALUED_1:def 11;
then A6: lim (f /* seq) = lim_in+infty f by A1, A3, Def12;
A7: f /* seq is convergent by A1, A3, A5;
then abs (f /* seq) is convergent ;
hence (abs f) /* seq is convergent by A5, RFUNCT_2:10; :: thesis: lim ((abs f) /* seq) = |.(lim_in+infty f).|
thus lim ((abs f) /* seq) = lim (abs (f /* seq)) by A5, RFUNCT_2:10
.= |.(lim_in+infty f).| by A7, A6, SEQ_4:14 ; :: thesis: verum

end;

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

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

end;

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