let X be RealUnitarySpace; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ( dist (seq,g) is convergent & lim (dist (seq,g)) = 0 )

hence ( dist (seq,g) is convergent & lim (dist (seq,g)) = 0 ) by A2, SEQ_2:def 7; :: thesis: verum

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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ( dist (seq,g) is convergent & lim (dist (seq,g)) = 0 )

A2: now :: thesis: 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).| < r

dist (seq,g) is convergent
by A1, Th23;ex k being Nat st

for n being Nat st n >= k holds

|.(((dist (seq,g)) . n) - 0).| < r

let r be Real; :: thesis: ( 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 ; :: thesis: ex k being Nat st

for n being Nat st n >= k holds

|.(((dist (seq,g)) . n) - 0).| < r

consider 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; :: thesis: for n being Nat st n >= k holds

|.(((dist (seq,g)) . n) - 0).| < r

let n be Nat; :: thesis: ( 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 ; :: thesis: |.(((dist (seq,g)) . n) - 0).| < r

then dist ((seq . n),g) < r by A4;

hence |.(((dist (seq,g)) . n) - 0).| < r by A5, Def4; :: thesis: verum

end;for n being Nat st n >= k holds

|.(((dist (seq,g)) . n) - 0).| < r )

assume A3: r > 0 ; :: thesis: ex k being Nat st

for n being Nat st n >= k holds

|.(((dist (seq,g)) . n) - 0).| < r

consider 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; :: thesis: for n being Nat st n >= k holds

|.(((dist (seq,g)) . n) - 0).| < r

let n be Nat; :: thesis: ( 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 ; :: thesis: |.(((dist (seq,g)) . n) - 0).| < r

then dist ((seq . n),g) < r by A4;

hence |.(((dist (seq,g)) . n) - 0).| < r by A5, Def4; :: thesis: verum

hence ( dist (seq,g) is convergent & lim (dist (seq,g)) = 0 ) by A2, SEQ_2:def 7; :: thesis: verum