let seq be Real_Sequence; :: thesis: ( ( seq is divergent_to+infty or seq is divergent_to-infty ) implies ( seq " is convergent & lim (seq " ) = 0 ) )
assume A1: ( seq is divergent_to+infty or seq is divergent_to-infty ) ; :: thesis: ( seq " is convergent & lim (seq " ) = 0 )

now

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

suppose A2: seq is divergent_to+infty ; :: thesis: ( seq " is convergent & seq " is convergent & lim (seq " ) = 0 )

A3: now

let r be real number ; :: thesis: ( 0 < r implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq " ) . m) - 0 ) < r )
assume A4: 0 < r ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq " ) . m) - 0 ) < r
r " is Real by XREAL_0:def 1;
then consider n being Element of NAT such that
A5: for m being Element of NAT st n <= m holds
r " < seq . m by A2, Def4;
take n = n; :: thesis: for m being Element of NAT st n <= m holds
abs (((seq " ) . m) - 0 ) < r
let m be Element of NAT ; :: thesis: ( n <= m implies abs (((seq " ) . m) - 0 ) < r )
assume n <= m ; :: thesis: abs (((seq " ) . m) - 0 ) < r
then A6: r " < seq . m by A5;
then 1 / (seq . m) < 1 / (r " ) by A4, XREAL_1:78;
then A7: 1 / (seq . m) < r by XCMPLX_1:218;
A8: ( 1 / (seq . m) = (seq . m) " & (seq . m) " = (seq " ) . m ) by VALUED_1:10, XCMPLX_1:217;
0 < r " by A4;
hence abs (((seq " ) . m) - 0 ) < r by A6, A7, A8, ABSVALUE:def 1; :: thesis: verum

end;

hence seq " is convergent by SEQ_2:def 6; :: thesis: ( seq " is convergent & lim (seq " ) = 0 )
hence ( seq " is convergent & lim (seq " ) = 0 ) by A3, SEQ_2:def 7; :: thesis: verum

end;

suppose A9: seq is divergent_to-infty ; :: thesis: ( seq " is convergent & seq " is convergent & lim (seq " ) = 0 )

A10: now

let r be real number ; :: thesis: ( 0 < r implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq " ) . m) - 0 ) < r )
assume A11: 0 < r ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq " ) . m) - 0 ) < r
A12: - (r " ) < - 0 by A11, XREAL_1:26;
- (r " ) is Real by XREAL_0:def 1;
then consider n being Element of NAT such that
A13: for m being Element of NAT st n <= m holds
seq . m < - (r " ) by A9, Def5;
take n = n; :: thesis: for m being Element of NAT st n <= m holds
abs (((seq " ) . m) - 0 ) < r
let m be Element of NAT ; :: thesis: ( n <= m implies abs (((seq " ) . m) - 0 ) < r )
assume A14: n <= m ; :: thesis: abs (((seq " ) . m) - 0 ) < r
then seq . m < - (r " ) by A13;
then 1 / (- (r " )) < 1 / (seq . m) by A12, XREAL_1:101;
then ((- 1) * (r " )) " < 1 / (seq . m) by XCMPLX_1:217;
then A15: ((- 1) " ) * ((r " ) " ) < 1 / (seq . m) by XCMPLX_1:205;
seq . m < - 0 by A11, A13, A14;
then 1 / (seq . m) < 0 / (seq . m) by XREAL_1:77;
then abs (1 / (seq . m)) = - (1 / (seq . m)) by ABSVALUE:def 1;
then - (1 * r) < - (abs (1 / (seq . m))) by A15;
then abs (1 / (seq . m)) < r by XREAL_1:26;
then abs ((seq . m) " ) < r by XCMPLX_1:217;
hence abs (((seq " ) . m) - 0 ) < r by VALUED_1:10; :: thesis: verum

end;

hence seq " is convergent by SEQ_2:def 6; :: thesis: ( seq " is convergent & lim (seq " ) = 0 )
hence ( seq " is convergent & lim (seq " ) = 0 ) by A10, SEQ_2:def 7; :: thesis: verum

end;

end;

end;

hence ( seq " is convergent & lim (seq " ) = 0 ) ; :: thesis: verum