let seq be Real_Sequence; :: thesis: ( ( seq is divergent_to+infty or seq is divergent_to-infty ) implies abs seq is divergent_to+infty )
assume A1: ( seq is divergent_to+infty or seq is divergent_to-infty ) ; :: thesis: abs seq is divergent_to+infty
let r be Real; :: according to LIMFUNC1:def 4 :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
r < (abs seq) . m

now

per cases ( seq is divergent_to+infty or seq is divergent_to-infty ) by A1;

suppose seq is divergent_to+infty ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
r < (abs seq) . m

then consider n being Element of NAT such that
A2: for m being Element of NAT st n <= m holds
abs r < seq . m by Def4;
take n = n; :: thesis: for m being Element of NAT st n <= m holds
r < (abs seq) . m
let m be Element of NAT ; :: thesis: ( n <= m implies r < (abs seq) . m )
assume n <= m ; :: thesis: r < (abs seq) . m
then ( r <= abs r & abs r < seq . m ) by A2, ABSVALUE:11;
then A3: r < seq . m by XXREAL_0:2;
seq . m <= abs (seq . m) by ABSVALUE:11;
then seq . m <= (abs seq) . m by SEQ_1:16;
hence r < (abs seq) . m by A3, XXREAL_0:2; :: thesis: verum

end;

suppose seq is divergent_to-infty ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
r < (abs seq) . m

then consider n being Element of NAT such that
A4: for m being Element of NAT st n <= m holds
seq . m < - r by Def5;
take n = n; :: thesis: for m being Element of NAT st n <= m holds
r < (abs seq) . m
let m be Element of NAT ; :: thesis: ( n <= m implies r < (abs seq) . m )
- (abs (seq . m)) <= seq . m by ABSVALUE:11;
then A5: - ((abs seq) . m) <= seq . m by SEQ_1:16;
assume n <= m ; :: thesis: r < (abs seq) . m
then seq . m < - r by A4;
then - ((abs seq) . m) < - r by A5, XXREAL_0:2;
hence r < (abs seq) . m by XREAL_1:26; :: thesis: verum

end;

end;

end;

hence ex n being Element of NAT st
for m being Element of NAT st n <= m holds
r < (abs seq) . m ; :: thesis: verum