let n be Nat; for s1 being sequence of (Euclid n)
for s2 being sequence of (REAL-NS n) st s1 = s2 holds
( s1 is Cauchy iff s2 is Cauchy_sequence_by_Norm )
let s1 be sequence of (Euclid n); for s2 being sequence of (REAL-NS n) st s1 = s2 holds
( s1 is Cauchy iff s2 is Cauchy_sequence_by_Norm )
let s2 be sequence of (REAL-NS n); ( s1 = s2 implies ( s1 is Cauchy iff s2 is Cauchy_sequence_by_Norm ) )
assume A1:
s1 = s2
; ( s1 is Cauchy iff s2 is Cauchy_sequence_by_Norm )
thus
( s1 is Cauchy implies s2 is Cauchy_sequence_by_Norm )
( s2 is Cauchy_sequence_by_Norm implies s1 is Cauchy )
assume A9:
s2 is Cauchy_sequence_by_Norm
; s1 is Cauchy
now for r being Real st r > 0 holds
( ex k being Nat st
for n0, m0 being Nat st k <= n0 & k <= m0 holds
dist ((s1 . n0),(s1 . m0)) < r & ex p being Nat st
for n, m being Nat st p <= n & p <= m holds
dist ((s1 . n),(s1 . m)) < r )let r be
Real;
( r > 0 implies ( ex k being Nat st
for n0, m0 being Nat st k <= n0 & k <= m0 holds
dist ((s1 . n0),(s1 . m0)) < r & ex p being Nat st
for n, m being Nat st p <= n & p <= m holds
dist ((s1 . n),(s1 . m)) < r ) )assume
r > 0
;
( ex k being Nat st
for n0, m0 being Nat st k <= n0 & k <= m0 holds
dist ((s1 . n0),(s1 . m0)) < r & ex p being Nat st
for n, m being Nat st p <= n & p <= m holds
dist ((s1 . n),(s1 . m)) < r )then consider k being
Nat such that A10:
for
n,
m being
Nat st
n >= k &
m >= k holds
||.((s2 . n) - (s2 . m)).|| < r
by A9, RSSPACE3:8;
hereby ex p being Nat st
for n, m being Nat st p <= n & p <= m holds
dist ((s1 . n),(s1 . m)) < r
take k =
k;
for n0, m0 being Nat st k <= n0 & k <= m0 holds
dist ((s1 . n0),(s1 . m0)) < r
end; hence
ex
p being
Nat st
for
n,
m being
Nat st
p <= n &
p <= m holds
dist (
(s1 . n),
(s1 . m))
< r
;
verum end;
hence
s1 is Cauchy
; verum