let f be PartFunc of REAL,REAL; :: thesis:
assume A1: ( f is divergent_in-infty_to+infty or f is divergent_in-infty_to-infty ) ; :: thesis:

now :: thesis:

per cases by A1;

suppose A2: f is divergent_in-infty_to+infty ; :: thesis:

A3: now :: thesis:

let seq be Real_Sequence; :: thesis:
assume that
A4: seq is divergent_to-infty and
A5: rng seq c= dom (abs f) ; :: thesis:
A6: rng seq c= dom f by A5, VALUED_1:def 11;
then f /* seq is divergent_to+infty by A2, A4;
then abs (f /* seq) is divergent_to+infty by Th25;
hence (abs f) /* seq is divergent_to+infty by A6, RFUNCT_2:10; :: thesis:

end;

now :: thesis:

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

end;

hence abs f is divergent_in-infty_to+infty by A3; :: thesis:

end;

suppose A8: f is divergent_in-infty_to-infty ; :: thesis:

A9: now :: thesis:

let seq be Real_Sequence; :: thesis:
assume that
A10: seq is divergent_to-infty and
A11: rng seq c= dom (abs f) ; :: thesis:
A12: rng seq c= dom f by A11, VALUED_1:def 11;
then f /* seq is divergent_to-infty by A8, A10;
then abs (f /* seq) is divergent_to+infty by Th25;
hence (abs f) /* seq is divergent_to+infty by A12, RFUNCT_2:10; :: thesis:

end;

now :: thesis:

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

end;

hence abs f is divergent_in-infty_to+infty by A9; :: thesis:

end;

end;

end;

hence abs f is divergent_in-infty_to+infty ; :: thesis: