let X be RealUnitarySpace; for g being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( dist (seq,g) is convergent & lim (dist (seq,g)) = 0 )
let g be Point of X; for seq being sequence of X st seq is convergent & lim seq = g holds
( dist (seq,g) is convergent & lim (dist (seq,g)) = 0 )
let seq be sequence of X; ( seq is convergent & lim seq = g implies ( dist (seq,g) is convergent & lim (dist (seq,g)) = 0 ) )
assume A1:
( seq is convergent & lim seq = g )
; ( dist (seq,g) is convergent & lim (dist (seq,g)) = 0 )
A2:
now for r being Real st r > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
|.(((dist (seq,g)) . n) - 0).| < rlet r be
Real;
( r > 0 implies ex k being Nat st
for n being Nat st n >= k holds
|.(((dist (seq,g)) . n) - 0).| < r )assume A3:
r > 0
;
ex k being Nat st
for n being Nat st n >= k holds
|.(((dist (seq,g)) . n) - 0).| < rconsider m1 being
Nat such that A4:
for
n being
Nat st
n >= m1 holds
dist (
(seq . n),
g)
< r
by A1, A3, Def2;
reconsider k =
m1 as
Nat ;
take k =
k;
for n being Nat st n >= k holds
|.(((dist (seq,g)) . n) - 0).| < rlet n be
Nat;
( n >= k implies |.(((dist (seq,g)) . n) - 0).| < r )
dist (
(seq . n),
g)
>= 0
by BHSP_1:37;
then A5:
|.((dist ((seq . n),g)) - 0).| = dist (
(seq . n),
g)
by ABSVALUE:def 1;
assume
n >= k
;
|.(((dist (seq,g)) . n) - 0).| < rthen
dist (
(seq . n),
g)
< r
by A4;
hence
|.(((dist (seq,g)) . n) - 0).| < r
by A5, Def4;
verum end;
dist (seq,g) is convergent
by A1, Th23;
hence
( dist (seq,g) is convergent & lim (dist (seq,g)) = 0 )
by A2, SEQ_2:def 7; verum