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 ) )

hence lim s = g by A7, SEQ_2:def 7; :: thesis: verum

( 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 A6:
( t is convergent & lim t = 0 )
; :: thesis: ( s is convergent & lim s = g )assume A2:
( s is convergent & lim s = g )
; :: thesis: ( t is convergent & lim t = 0 )

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

end;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

hence
t is convergent
by SEQ_2:def 6; :: thesis: lim t = 0 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

|.((t . m) - 0).| < r ; :: thesis: verum

end;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

hence
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;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

|.((t . m) - 0).| < r ; :: thesis: verum

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

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

hence
s is convergent
by SEQ_2:def 6; :: thesis: lim s = gex 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

|.((s . m) - g).| < r ; :: thesis: verum

end;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

hence
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;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

|.((s . m) - g).| < r ; :: thesis: verum

hence lim s = g by A7, SEQ_2:def 7; :: thesis: verum