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

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

let seq be sequence of X; :: thesis: ( seq is convergent & lim seq = g implies dist (seq,g) is convergent )

assume A1: ( seq is convergent & lim seq = g ) ; :: thesis: dist (seq,g) is convergent

for seq being sequence of X st seq is convergent & lim seq = g holds

dist (seq,g) is convergent

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

let seq be sequence of X; :: thesis: ( seq is convergent & lim seq = g implies dist (seq,g) is convergent )

assume A1: ( seq is convergent & lim seq = g ) ; :: thesis: dist (seq,g) is convergent

now :: thesis: for r being Real st r > 0 holds

ex k being Nat st

for n being Nat st k <= n holds

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

hence
dist (seq,g) is convergent
by SEQ_2:def 6; :: thesis: verumex k being Nat st

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

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

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

for n being Nat st k <= n holds

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

consider m1 being Nat such that

A3: for n being Nat st n >= m1 holds

dist ((seq . n),g) < r by A1, A2, Def2;

reconsider k = m1 as Nat ;

take k = k; :: thesis: for n being Nat st k <= n holds

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

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

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

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

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

for n being Nat st k <= n holds

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

consider m1 being Nat such that

A3: for n being Nat st n >= m1 holds

dist ((seq . n),g) < r by A1, A2, Def2;

reconsider k = m1 as Nat ;

take k = k; :: thesis: for n being Nat st k <= n holds

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

now :: thesis: for n being Nat st n >= k holds

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

hence
for n being Nat st k <= n 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 A4: |.((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 A3;

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

end;dist ((seq . n),g) >= 0 by BHSP_1:37;

then A4: |.((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 A3;

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

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