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 :: thesis: abs f is divergent_in+infty_to+infty

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 :: thesis: for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom (abs f) holds
(abs f) /* seq is divergent_to+infty

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;
then |.(f /* seq).| is divergent_to+infty by Th25;
hence (abs f) /* seq is divergent_to+infty by A6, RFUNCT_2:10; :: 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
A7: ( r < g & g in dom f ) by A2;
take g = g; :: thesis: ( r < g & g in dom (abs f) )
thus ( r < g & 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; :: thesis: verum

end;

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

A9: now :: thesis: for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom (abs f) holds
(abs f) /* seq is divergent_to+infty

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;
then |.(f /* seq).| is divergent_to+infty by Th25;
hence (abs f) /* seq is divergent_to+infty by A12, RFUNCT_2:10; :: 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
A13: ( r < g & g in dom f ) by A8;
take g = g; :: thesis: ( r < g & g in dom (abs f) )
thus ( r < g & 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; :: thesis: verum

end;

end;

end;

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