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

let r be real number ; :: thesis: ( r > 0 implies ex k being Element of NAT st
for n being Element of NAT st k <= n holds
abs (((dist (seq,g)) . n) - 0) < r )
assume A2: r > 0 ; :: thesis: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
abs (((dist (seq,g)) . n) - 0) < r
r is Real by XREAL_0:def 1;
then consider m1 being Element of NAT such that
A3: for n being Element of NAT st n >= m1 holds
dist ((seq . n),g) < r by A1, A2, Def2;
take k = m1; :: thesis: for n being Element of NAT st k <= n holds
abs (((dist (seq,g)) . n) - 0) < r

now

let n be Element of NAT ; :: thesis: ( n >= k implies abs (((dist (seq,g)) . n) - 0) < r )
dist ((seq . n),g) >= 0 by CSSPACE:53;
then A4: abs ((dist ((seq . n),g)) - 0) = dist ((seq . n),g) by ABSVALUE:def 1;
assume n >= k ; :: thesis: abs (((dist (seq,g)) . n) - 0) < r
then dist ((seq . n),g) < r by A3;
hence abs (((dist (seq,g)) . n) - 0) < r by A4, Def4; :: thesis: verum

end;

hence for n being Element of NAT st k <= n holds
abs (((dist (seq,g)) . n) - 0) < r ; :: thesis: verum

end;

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