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
( ||.(seq - g).|| is convergent & lim ||.(seq - g).|| = 0 )
let g be Point of X; :: thesis: for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(seq - g).|| is convergent & lim ||.(seq - g).|| = 0 )
let seq be sequence of X; :: thesis: ( seq is convergent & lim seq = g implies ( ||.(seq - g).|| is convergent & lim ||.(seq - g).|| = 0 ) )
assume that
A1: seq is convergent and
A2: lim seq = g ; :: thesis: ( ||.(seq - g).|| is convergent & lim ||.(seq - g).|| = 0 )

A3: 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 ((||.(seq - g).|| . n) - 0) < r )
assume A4: r > 0 ; :: thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs ((||.(seq - g).|| . n) - 0) < r
r is Real by XREAL_0:def 1;
then consider m1 being Element of NAT such that
A5: for n being Element of NAT st n >= m1 holds
||.((seq . n) - g).|| < r by A1, A2, A4, Th19;
take k = m1; :: thesis: for n being Element of NAT st n >= k holds
abs ((||.(seq - g).|| . n) - 0) < r
let n be Element of NAT ; :: thesis: ( n >= k implies abs ((||.(seq - g).|| . n) - 0) < r )
assume n >= k ; :: thesis: abs ((||.(seq - g).|| . n) - 0) < r
then ||.((seq . n) - g).|| < r by A5;
then A6: ||.(((seq . n) - g) - H₁(X)).|| < r by RLVECT_1:13;
abs (||.((seq . n) - g).|| - ||.H₁(X).||) <= ||.(((seq . n) - g) - H₁(X)).|| by BHSP_1:33;
then abs (||.((seq . n) - g).|| - ||.H₁(X).||) < r by A6, XXREAL_0:2;
then abs (||.((seq . n) - g).|| - 0) < r by BHSP_1:26;
then abs (||.((seq - g) . n).|| - 0) < r by NORMSP_1:def 4;
hence abs ((||.(seq - g).|| . n) - 0) < r by Def3; :: thesis: verum

end;

||.(seq - g).|| is convergent by A1, Th8, Th20;
hence ( ||.(seq - g).|| is convergent & lim ||.(seq - g).|| = 0 ) by A3, SEQ_2:def 7; :: thesis: verum