let x0 be Real; :: thesis: for f being PartFunc of REAL,REAL st ( f is_left_divergent_to+infty_in x0 or f is_left_divergent_to-infty_in x0 ) holds
abs f is_left_divergent_to+infty_in x0
let f be PartFunc of REAL,REAL; :: thesis: ( ( f is_left_divergent_to+infty_in x0 or f is_left_divergent_to-infty_in x0 ) implies abs f is_left_divergent_to+infty_in x0 )
assume A1: ( f is_left_divergent_to+infty_in x0 or f is_left_divergent_to-infty_in x0 ) ; :: thesis: abs f is_left_divergent_to+infty_in x0

now :: thesis: abs f is_left_divergent_to+infty_in x0

per cases ( f is_left_divergent_to+infty_in x0 or f is_left_divergent_to-infty_in x0 ) by A1;

suppose A2: f is_left_divergent_to+infty_in x0 ; :: thesis: abs f is_left_divergent_to+infty_in x0

A3: now :: thesis: for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom (abs f)) /\ (left_open_halfline x0) holds
(abs f) /* seq is divergent_to+infty

let seq be Real_Sequence; :: thesis: ( seq is convergent & lim seq = x0 & rng seq c= (dom (abs f)) /\ (left_open_halfline x0) implies (abs f) /* seq is divergent_to+infty )
assume that
A4: seq is convergent and
A5: lim seq = x0 and
A6: rng seq c= (dom (abs f)) /\ (left_open_halfline x0) ; :: thesis: (abs f) /* seq is divergent_to+infty
A7: rng seq c= (dom f) /\ (left_open_halfline x0) by A6, VALUED_1:def 11;
then f /* seq is divergent_to+infty by A2, A4, A5;
then A8: abs (f /* seq) is divergent_to+infty by LIMFUNC1:25;
(dom f) /\ (left_open_halfline x0) c= dom f by XBOOLE_1:17;
then rng seq c= dom f by A7, XBOOLE_1:1;
hence (abs f) /* seq is divergent_to+infty by A8, RFUNCT_2:10; :: thesis: verum

end;

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

let r be Real; :: thesis: ( r < x0 implies ex g being Real st
( r < g & g < x0 & g in dom (abs f) ) )
assume r < x0 ; :: thesis: ex g being Real st
( r < g & g < x0 & g in dom (abs f) )
then consider g being Real such that
A9: r < g and
A10: g < x0 and
A11: g in dom f by A2;
take g = g; :: thesis: ( r < g & g < x0 & g in dom (abs f) )
thus ( r < g & g < x0 & g in dom (abs f) ) by A9, A10, A11, VALUED_1:def 11; :: thesis: verum

end;

hence abs f is_left_divergent_to+infty_in x0 by A3; :: thesis: verum

end;

suppose A12: f is_left_divergent_to-infty_in x0 ; :: thesis: abs f is_left_divergent_to+infty_in x0

A13: now :: thesis: for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom (abs f)) /\ (left_open_halfline x0) holds
(abs f) /* seq is divergent_to+infty

let seq be Real_Sequence; :: thesis: ( seq is convergent & lim seq = x0 & rng seq c= (dom (abs f)) /\ (left_open_halfline x0) implies (abs f) /* seq is divergent_to+infty )
assume that
A14: seq is convergent and
A15: lim seq = x0 and
A16: rng seq c= (dom (abs f)) /\ (left_open_halfline x0) ; :: thesis: (abs f) /* seq is divergent_to+infty
A17: rng seq c= (dom f) /\ (left_open_halfline x0) by A16, VALUED_1:def 11;
then f /* seq is divergent_to-infty by A12, A14, A15;
then A18: abs (f /* seq) is divergent_to+infty by LIMFUNC1:25;
(dom f) /\ (left_open_halfline x0) c= dom f by XBOOLE_1:17;
then rng seq c= dom f by A17, XBOOLE_1:1;
hence (abs f) /* seq is divergent_to+infty by A18, RFUNCT_2:10; :: thesis: verum

end;

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

let r be Real; :: thesis: ( r < x0 implies ex g being Real st
( r < g & g < x0 & g in dom (abs f) ) )
assume r < x0 ; :: thesis: ex g being Real st
( r < g & g < x0 & g in dom (abs f) )
then consider g being Real such that
A19: r < g and
A20: g < x0 and
A21: g in dom f by A12;
take g = g; :: thesis: ( r < g & g < x0 & g in dom (abs f) )
thus ( r < g & g < x0 & g in dom (abs f) ) by A19, A20, A21, VALUED_1:def 11; :: thesis: verum

end;

hence abs f is_left_divergent_to+infty_in x0 by A13; :: thesis: verum

end;

end;

end;

hence abs f is_left_divergent_to+infty_in x0 ; :: thesis: verum