let s, t be Real_Sequence; :: thesis: for g being Real st ( for n being Element of NAT holds t . n = |.((s . n) - g).| ) holds
( s is convergent & lim s = g iff ( t is convergent & lim t = 0 ) )

let g be Real; :: thesis: ( ( for n being Element of NAT holds t . n = |.((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 = |.((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 :: thesis: for r being Real st 0 < r holds
ex n being Nat st
for m being Nat st n <= m holds
|.((t . m) - 0).| < r
let r be Real; :: thesis: ( 0 < r implies ex n being Nat st
for m being Nat st n <= m holds
|.((t . m) - 0).| < r )

assume 0 < r ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((t . m) - 0).| < r

then consider n being Nat such that
A4: for m being Nat st n <= m holds
|.((s . m) - g).| < r by ;
take n = n; :: thesis: for m being Nat st n <= m holds
|.((t . m) - 0).| < r

now :: thesis: for m being Nat st n <= m holds
|.((t . m) - 0).| < r
let m be Nat; :: thesis: ( n <= m implies |.((t . m) - 0).| < r )
A5: m in NAT by ORDINAL1:def 12;
assume n <= m ; :: thesis: |.((t . m) - 0).| < r
then |.|.((s . m) - g).|.| < r by A4;
hence |.((t . m) - 0).| < r by A1, A5; :: thesis: verum
end;
hence for m being Nat st n <= m holds
|.((t . m) - 0).| < r ; :: thesis: verum
end;
hence t is convergent by SEQ_2:def 6; :: thesis:
hence lim t = 0 by ; :: thesis: verum
end;
assume A6: ( t is convergent & lim t = 0 ) ; :: thesis: ( s is convergent & lim s = g )
A7: now :: thesis: for r being Real st 0 < r holds
ex n being Nat st
for m being Nat st n <= m holds
|.((s . m) - g).| < r
let r be Real; :: thesis: ( 0 < r implies ex n being Nat st
for m being Nat st n <= m holds
|.((s . m) - g).| < r )

assume 0 < r ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((s . m) - g).| < r

then consider n being Nat such that
A8: for m being Nat st n <= m holds
|.((t . m) - 0).| < r by ;
take n = n; :: thesis: for m being Nat st n <= m holds
|.((s . m) - g).| < r

now :: thesis: for m being Nat st n <= m holds
|.((s . m) - g).| < r
let m be Nat; :: thesis: ( n <= m implies |.((s . m) - g).| < r )
A9: m in NAT by ORDINAL1:def 12;
assume n <= m ; :: thesis: |.((s . m) - g).| < r
then |.((t . m) - 0).| < r by A8;
then |.|.((s . m) - g).|.| < r by A1, A9;
hence |.((s . m) - g).| < r ; :: thesis: verum
end;
hence for m being Nat st n <= m holds
|.((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 ; :: thesis: verum