let X be RealNormSpace; :: thesis: for Sq being sequence of X
for Sq0 being Point of X
for R1 being Real_Sequence
for N being V174() sequence of NAT st Sq is Cauchy_sequence_by_Norm & ( for i being Nat holds R1 . i = ||.(Sq0 - (Sq . (N . i))).|| ) & R1 is convergent & lim R1 = 0 holds
( Sq is convergent & lim Sq = Sq0 & ||.(Sq - Sq0).|| is convergent & lim ||.(Sq - Sq0).|| = 0 )

let Sq be sequence of X; :: thesis: for Sq0 being Point of X
for R1 being Real_Sequence
for N being V174() sequence of NAT st Sq is Cauchy_sequence_by_Norm & ( for i being Nat holds R1 . i = ||.(Sq0 - (Sq . (N . i))).|| ) & R1 is convergent & lim R1 = 0 holds
( Sq is convergent & lim Sq = Sq0 & ||.(Sq - Sq0).|| is convergent & lim ||.(Sq - Sq0).|| = 0 )

let Sq0 be Point of X; :: thesis: for R1 being Real_Sequence
for N being V174() sequence of NAT st Sq is Cauchy_sequence_by_Norm & ( for i being Nat holds R1 . i = ||.(Sq0 - (Sq . (N . i))).|| ) & R1 is convergent & lim R1 = 0 holds
( Sq is convergent & lim Sq = Sq0 & ||.(Sq - Sq0).|| is convergent & lim ||.(Sq - Sq0).|| = 0 )

let R1 be Real_Sequence; :: thesis: for N being V174() sequence of NAT st Sq is Cauchy_sequence_by_Norm & ( for i being Nat holds R1 . i = ||.(Sq0 - (Sq . (N . i))).|| ) & R1 is convergent & lim R1 = 0 holds
( Sq is convergent & lim Sq = Sq0 & ||.(Sq - Sq0).|| is convergent & lim ||.(Sq - Sq0).|| = 0 )

let N be V174() sequence of NAT; :: thesis: ( Sq is Cauchy_sequence_by_Norm & ( for i being Nat holds R1 . i = ||.(Sq0 - (Sq . (N . i))).|| ) & R1 is convergent & lim R1 = 0 implies ( Sq is convergent & lim Sq = Sq0 & ||.(Sq - Sq0).|| is convergent & lim ||.(Sq - Sq0).|| = 0 ) )
assume that
A1: Sq is Cauchy_sequence_by_Norm and
A2: for i being Nat holds R1 . i = ||.(Sq0 - (Sq . (N . i))).|| and
A3: ( R1 is convergent & lim R1 = 0 ) ; :: thesis: ( Sq is convergent & lim Sq = Sq0 & ||.(Sq - Sq0).|| is convergent & lim ||.(Sq - Sq0).|| = 0 )
A4: now :: thesis: for p being Real st 0 < p holds
ex n3 being Nat st
for n being Nat st n3 <= n holds
||.((Sq . n) - Sq0).|| < p
let p be Real; :: thesis: ( 0 < p implies ex n3 being Nat st
for n being Nat st n3 <= n holds
||.((Sq . n) - Sq0).|| < p )

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

then consider n2 being Nat such that
A6: for m, n being Nat st n2 <= m & n2 <= n holds
||.((Sq . m) - (Sq . n)).|| < p / 2 by ;
consider n1 being Nat such that
A7: for l being Nat st n1 <= l holds
|.((R1 . l) - 0).| < p / 2 by ;
reconsider n3 = max (n1,n2) as Nat by TARSKI:1;
take n3 = n3; :: thesis: for n being Nat st n3 <= n holds
||.((Sq . n) - Sq0).|| < p

thus for n being Nat st n3 <= n holds
||.((Sq . n) - Sq0).|| < p :: thesis: verum
proof
let n be Nat; :: thesis: ( n3 <= n implies ||.((Sq . n) - Sq0).|| < p )
assume A8: n3 <= n ; :: thesis: ||.((Sq . n) - Sq0).|| < p
n1 <= n3 by XXREAL_0:25;
then n1 <= n by ;
then |.((R1 . n) - 0).| < p / 2 by A7;
then A9: |.||.(Sq0 - (Sq . (N . n))).||.| < p / 2 by A2;
A10: ||.(Sq0 - (Sq . (N . n))).|| < p / 2 by ;
n <= N . n by SEQM_3:14;
then A11: n3 <= N . n by ;
n2 <= n3 by XXREAL_0:25;
then ( n2 <= N . n & n2 <= n ) by ;
then ||.((Sq . (N . n)) - (Sq . n)).|| < p / 2 by A6;
then A12: ||.(Sq0 - (Sq . (N . n))).|| + ||.((Sq . (N . n)) - (Sq . n)).|| < (p / 2) + (p / 2) by ;
A13: ||.((Sq . n) - Sq0).|| = ||.(Sq0 - (Sq . n)).|| by NORMSP_1:7
.= ||.((Sq0 - (Sq . (N . n))) + ((Sq . (N . n)) - (Sq . n))).|| by LOPBAN_3:3 ;
||.((Sq0 - (Sq . (N . n))) + ((Sq . (N . n)) - (Sq . n))).|| <= ||.(Sq0 - (Sq . (N . n))).|| + ||.((Sq . (N . n)) - (Sq . n)).|| by NORMSP_1:def 1;
hence ||.((Sq . n) - Sq0).|| < p by ; :: thesis: verum
end;
end;
hence A14: Sq is convergent by NORMSP_1:def 6; :: thesis: ( lim Sq = Sq0 & ||.(Sq - Sq0).|| is convergent & lim ||.(Sq - Sq0).|| = 0 )
hence lim Sq = Sq0 by ; :: thesis: ( ||.(Sq - Sq0).|| is convergent & lim ||.(Sq - Sq0).|| = 0 )
hence ( ||.(Sq - Sq0).|| is convergent & lim ||.(Sq - Sq0).|| = 0 ) by ; :: thesis: verum