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 A2, SEQ_2:def 7;
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: lim t = 0
hence lim t = 0 by A3, SEQ_2:def 7; :: 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 A6, SEQ_2:def 7;
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 A7, SEQ_2:def 7; :: thesis: verum