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 )

hence lim Sq = Sq0 by A4, NORMSP_1:def 7; :: thesis: ( ||.(Sq - Sq0).|| is convergent & lim ||.(Sq - Sq0).|| = 0 )

hence ( ||.(Sq - Sq0).|| is convergent & lim ||.(Sq - Sq0).|| = 0 ) by A14, NORMSP_1:24; :: thesis: verum

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

hence A14:
Sq is convergent
by NORMSP_1:def 6; :: thesis: ( lim Sq = Sq0 & ||.(Sq - Sq0).|| is convergent & lim ||.(Sq - Sq0).|| = 0 )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 A1, RSSPACE3:8;

consider n1 being Nat such that

A7: for l being Nat st n1 <= l holds

|.((R1 . l) - 0).| < p / 2 by A3, A5, SEQ_2:def 7;

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

end;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 A1, RSSPACE3:8;

consider n1 being Nat such that

A7: for l being Nat st n1 <= l holds

|.((R1 . l) - 0).| < p / 2 by A3, A5, SEQ_2:def 7;

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 A8, XXREAL_0:2;

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 A9, ABSVALUE:def 1;

n <= N . n by SEQM_3:14;

then A11: n3 <= N . n by A8, XXREAL_0:2;

n2 <= n3 by XXREAL_0:25;

then ( n2 <= N . n & n2 <= n ) by A8, A11, XXREAL_0:2;

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 A10, XREAL_1:8;

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 A13, A12, XXREAL_0:2; :: thesis: verum

end;assume A8: n3 <= n ; :: thesis: ||.((Sq . n) - Sq0).|| < p

n1 <= n3 by XXREAL_0:25;

then n1 <= n by A8, XXREAL_0:2;

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 A9, ABSVALUE:def 1;

n <= N . n by SEQM_3:14;

then A11: n3 <= N . n by A8, XXREAL_0:2;

n2 <= n3 by XXREAL_0:25;

then ( n2 <= N . n & n2 <= n ) by A8, A11, XXREAL_0:2;

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 A10, XREAL_1:8;

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 A13, A12, XXREAL_0:2; :: thesis: verum

hence lim Sq = Sq0 by A4, NORMSP_1:def 7; :: thesis: ( ||.(Sq - Sq0).|| is convergent & lim ||.(Sq - Sq0).|| = 0 )

hence ( ||.(Sq - Sq0).|| is convergent & lim ||.(Sq - Sq0).|| = 0 ) by A14, NORMSP_1:24; :: thesis: verum