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