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 A1, SEQ_2:def 7;
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 A2, NORMSP_1:def 7; :: thesis: verum