let seq1 be sequence of RNS_Real; :: thesis: ( seq1 is Cauchy_sequence_by_Norm implies seq1 is convergent )
assume AS: seq1 is Cauchy_sequence_by_Norm ; :: thesis: seq1 is convergent
reconsider seq = seq1 as Real_Sequence ;
for s being Real st 0 < s holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (seq . n)).| < s
proof
let s be Real; :: thesis: ( 0 < s implies ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (seq . n)).| < s )
assume 0 < s ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (seq . n)).| < s
then consider k being Nat such that
P1: for n, m being Nat st n >= k & m >= k holds
||.((seq1 . n) - (seq1 . m)).|| < s by AS, RSSPACE3:8;
take k ; :: thesis: for m being Nat st k <= m holds
|.((seq . m) - (seq . k)).| < s
hereby :: thesis: verum
let m be Nat; :: thesis: ( k <= m implies |.((seq . m) - (seq . k)).| < s )
assume k <= m ; :: thesis: |.((seq . m) - (seq . k)).| < s
then P2: ||.((seq1 . m) - (seq1 . k)).|| < s by P1;
(seq1 . m) - (seq1 . k) = (seq . m) - (seq . k) by RNS4;
hence |.((seq . m) - (seq . k)).| < s by EUCLID:def 2, P2; :: thesis: verum
end;
end;
then seq is convergent by SEQ_4:41;
hence seq1 is convergent by RNS8; :: thesis: verum