let s, t be Real_Sequence; :: thesis: for g being real number st ( for n being Element of NAT holds t . n = abs ((s . n) - g) ) holds
( s is convergent & lim s = g iff ( t is convergent & lim t = 0 ) )
let g be real number ; :: thesis: ( ( for n being Element of NAT holds t . n = abs ((s . n) - g) ) implies ( s is convergent & lim s = g iff ( t is convergent & lim t = 0 ) ) )
assume A1: for n being Element of NAT holds t . n = abs ((s . n) - g) ; :: thesis: ( s is convergent & lim s = g iff ( t is convergent & lim t = 0 ) )

hereby :: thesis: ( t is convergent & lim t = 0 implies ( s is convergent & lim s = g ) )

assume A2: ( s is convergent & lim s = g ) ; :: thesis: ( t is convergent & lim t = 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 ((t . m) - 0) < r )
assume 0 < r ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((t . m) - 0) < r
then consider n being Element of NAT such that
A4: for m being Element of NAT st n <= m holds
abs ((s . m) - g) < r by A2, SEQ_2:def 7;
take n = n; :: thesis: for m being Element of NAT st n <= m holds
abs ((t . m) - 0) < r

now

let m be Element of NAT ; :: thesis: ( n <= m implies abs ((t . m) - 0) < r )
assume n <= m ; :: thesis: abs ((t . m) - 0) < r
then abs (abs ((s . m) - g)) < r by A4;
hence abs ((t . m) - 0) < r by A1; :: thesis: verum

end;

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

end;

hence t is convergent by SEQ_2:def 6; :: thesis: lim t = 0
hence lim t = 0 by A3, SEQ_2:def 7; :: thesis: verum

end;

assume A5: ( t is convergent & lim t = 0 ) ; :: thesis: ( s is convergent & lim s = g )

A6: 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 ((s . m) - g) < r )
assume 0 < r ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((s . m) - g) < r
then consider n being Element of NAT such that
A7: for m being Element of NAT st n <= m holds
abs ((t . m) - 0) < r by A5, SEQ_2:def 7;
take n = n; :: thesis: for m being Element of NAT st n <= m holds
abs ((s . m) - g) < r

now

let m be Element of NAT ; :: thesis: ( n <= m implies abs ((s . m) - g) < r )
assume n <= m ; :: thesis: abs ((s . m) - g) < r
then abs ((t . m) - 0) < r by A7;
then abs (abs ((s . m) - g)) < r by A1;
hence abs ((s . m) - g) < r ; :: thesis: verum

end;

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

end;

hence s is convergent by SEQ_2:def 6; :: thesis: lim s = g
hence lim s = g by A6, SEQ_2:def 7; :: thesis: verum