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

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 k <= n holds
abs ((||.seq.|| . n) - ||.g.||) < r )
assume A4: r > 0 ; :: thesis: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
abs ((||.seq.|| . n) - ||.g.||) < 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 k <= n holds
abs ((||.seq.|| . n) - ||.g.||) < r

now

let n be Element of NAT ; :: thesis: ( n >= k implies abs ((||.seq.|| . n) - ||.g.||) < r )
assume n >= k ; :: thesis: abs ((||.seq.|| . n) - ||.g.||) < r
then A6: ||.((seq . n) - g).|| < r by A5;
abs (||.(seq . n).|| - ||.g.||) <= ||.((seq . n) - g).|| by BHSP_1:33;
then abs (||.(seq . n).|| - ||.g.||) < r by A6, XXREAL_0:2;
hence abs ((||.seq.|| . n) - ||.g.||) < r by Def3; :: thesis: verum

end;

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

end;

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