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 r be Real; :: thesis: ex g being Real st
( g < r & g in dom (abs f) )
consider g being Real such that
A4: ( 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 A4, VALUED_1:def 11; :: thesis: verum

end;

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 A5: ( seq is divergent_to-infty & rng seq c= dom (abs f) ) ; :: thesis: (abs f) /* seq is divergent_to+infty
then A6: rng seq c= dom f by VALUED_1:def 11;
then f /* seq is divergent_to+infty by A2, A5, Def10;
then abs (f /* seq) is divergent_to+infty by Th52;
hence (abs f) /* seq is divergent_to+infty by A6, RFUNCT_2:25; :: thesis: verum

end;

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

end;

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

A8: now

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

end;

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 A10: ( seq is divergent_to-infty & rng seq c= dom (abs f) ) ; :: thesis: (abs f) /* seq is divergent_to+infty
then A11: rng seq c= dom f by VALUED_1:def 11;
then f /* seq is divergent_to-infty by A7, A10, Def11;
then abs (f /* seq) is divergent_to+infty by Th52;
hence (abs f) /* seq is divergent_to+infty by A11, RFUNCT_2:25; :: thesis: verum

end;

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

end;

end;

end;

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