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 that
A1: seq is convergent and
A2: lim seq = g ; :: thesis: ( dist seq,g is convergent & lim (dist seq,g) = 0 )
A3: dist seq,g is convergent by A1, A2, Th23;

now

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

end;

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