let x0 be Real; :: thesis:
let f be PartFunc of REAL,REAL; :: thesis:
assume A1: ( f is_divergent_to+infty_in x0 or f is_divergent_to-infty_in x0 ) ; :: thesis:

now :: thesis:

per cases by A1;

suppose A2: f is_divergent_to+infty_in x0 ; :: thesis:

A3: now :: thesis:

let seq be Real_Sequence; :: thesis:
assume that
A4: seq is convergent and
A5: lim seq = x0 and
A6: rng seq c= (dom (abs f)) \ {x0} ; :: thesis:
A7: rng seq c= (dom f) \ {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;
rng seq c= dom f by A7, XBOOLE_1:1;
hence (abs f) /* seq is divergent_to+infty by A8, RFUNCT_2:10; :: thesis:

end;

now :: thesis:

let r1, r2 be Real; :: thesis:
assume that
A9: r1 < x0 and
A10: x0 < r2 ; :: thesis:
consider g1, g2 being Real such that
A11: r1 < g1 and
A12: g1 < x0 and
A13: g1 in dom f and
A14: g2 < r2 and
A15: x0 < g2 and
A16: g2 in dom f by A2, A9, A10;
take g1 = g1; :: thesis:
take g2 = g2; :: thesis:
thus ( r1 < g1 & g1 < x0 & g1 in dom (abs f) & g2 < r2 & x0 < g2 & g2 in dom (abs f) ) by A11, A12, A13, A14, A15, A16, VALUED_1:def 11; :: thesis:

end;

hence abs f is_divergent_to+infty_in x0 by A3; :: thesis:

end;

suppose A17: f is_divergent_to-infty_in x0 ; :: thesis:

A18: now :: thesis:

let seq be Real_Sequence; :: thesis:
assume that
A19: seq is convergent and
A20: lim seq = x0 and
A21: rng seq c= (dom (abs f)) \ {x0} ; :: thesis:
A22: rng seq c= (dom f) \ {x0} by A21, VALUED_1:def 11;
then f /* seq is divergent_to-infty by A17, A19, A20;
then A23: abs (f /* seq) is divergent_to+infty by LIMFUNC1:25;
rng seq c= dom f by A22, XBOOLE_1:1;
hence (abs f) /* seq is divergent_to+infty by A23, RFUNCT_2:10; :: thesis:

end;

now :: thesis:

let r1, r2 be Real; :: thesis:
assume that
A24: r1 < x0 and
A25: x0 < r2 ; :: thesis:
consider g1, g2 being Real such that
A26: r1 < g1 and
A27: g1 < x0 and
A28: g1 in dom f and
A29: g2 < r2 and
A30: x0 < g2 and
A31: g2 in dom f by A17, A24, A25;
take g1 = g1; :: thesis:
take g2 = g2; :: thesis:
thus ( r1 < g1 & g1 < x0 & g1 in dom (abs f) & g2 < r2 & x0 < g2 & g2 in dom (abs f) ) by A26, A27, A28, A29, A30, A31, VALUED_1:def 11; :: thesis:

end;

hence abs f is_divergent_to+infty_in x0 by A18; :: thesis:

end;

end;

end;

hence abs f is_divergent_to+infty_in x0 ; :: thesis: