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

now

per cases ( f is divergent_in-infty_to+infty or f is divergent_in-infty_to-infty ) by A1;

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

A3: now

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

end;

now

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

end;

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

end;

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

A9: now

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

end;

now

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

end;

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

end;

end;

end;

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