let X be ComplexUnitarySpace; :: 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

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

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;
take k = m1; :: 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

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

hence for n being Nat st k <= n holds
|.(((dist (seq,g)) . n) - 0).| < r ; :: thesis: verum

end;

hence dist (seq,g) is convergent by SEQ_2:def 6; :: thesis: verum