let X be RealNormSpace; :: thesis: for Sq being sequence of X
for Sq0 being Point of X st ||.(Sq - Sq0).|| is convergent & lim ||.(Sq - Sq0).|| = 0 holds
( Sq is convergent & lim Sq = Sq0 )

let Sq be sequence of X; :: thesis: for Sq0 being Point of X st ||.(Sq - Sq0).|| is convergent & lim ||.(Sq - Sq0).|| = 0 holds
( Sq is convergent & lim Sq = Sq0 )

let Sq0 be Point of X; :: thesis: ( ||.(Sq - Sq0).|| is convergent & lim ||.(Sq - Sq0).|| = 0 implies ( Sq is convergent & lim Sq = Sq0 ) )
assume A1: ( ||.(Sq - Sq0).|| is convergent & lim ||.(Sq - Sq0).|| = 0 ) ; :: thesis: ( Sq is convergent & lim Sq = Sq0 )
A2: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
||.((Sq . m) - Sq0).|| < p
proof
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
||.((Sq . m) - Sq0).|| < p )

assume 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
||.((Sq . m) - Sq0).|| < p

then consider n being Nat such that
A3: for m being Nat st n <= m holds
|.((||.(Sq - Sq0).|| . m) - 0).| < p by ;
take n ; :: thesis: for m being Nat st n <= m holds
||.((Sq . m) - Sq0).|| < p

hereby :: thesis: verum
let m be Nat; :: thesis: ( n <= m implies ||.((Sq . m) - Sq0).|| < p )
assume n <= m ; :: thesis: ||.((Sq . m) - Sq0).|| < p
then |.((||.(Sq - Sq0).|| . m) - 0).| < p by A3;
then |.||.((Sq - Sq0) . m).||.| < p by NORMSP_0:def 4;
then |.||.((Sq . m) - Sq0).||.| < p by NORMSP_1:def 4;
hence ||.((Sq . m) - Sq0).|| < p by ABSVALUE:def 1; :: thesis: verum
end;
end;
hence Sq is convergent by NORMSP_1:def 6; :: thesis: lim Sq = Sq0
hence lim Sq = Sq0 by ; :: thesis: verum