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

hence lim Sq = Sq0 by A2, NORMSP_1:def 7; :: thesis: verum

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

hence
Sq is convergent
by NORMSP_1:def 6; :: thesis: lim Sq = Sq0
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

end;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;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

hence lim Sq = Sq0 by A2, NORMSP_1:def 7; :: thesis: verum