let n be Nat; :: thesis: 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); :: thesis: 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); :: thesis: ( s1 = s2 implies ( s1 is Cauchy iff s2 is Cauchy_sequence_by_Norm ) )
assume A1: s1 = s2 ; :: thesis: ( s1 is Cauchy iff s2 is Cauchy_sequence_by_Norm )
thus ( s1 is Cauchy implies s2 is Cauchy_sequence_by_Norm ) :: thesis: ( s2 is Cauchy_sequence_by_Norm implies s1 is Cauchy )
proof
assume A3: s1 is Cauchy ; :: thesis: s2 is Cauchy_sequence_by_Norm
now :: thesis: for r being Real st r > 0 holds
ex p being Nat st
for n0, m0 being Nat st n0 >= p & m0 >= p holds
||.((s2 . n0) - (s2 . m0)).|| < r
let r be Real; :: thesis: ( r > 0 implies ex p being Nat st
for n0, m0 being Nat st n0 >= p & m0 >= p holds
||.((s2 . n0) - (s2 . m0)).|| < r )
assume r > 0 ; :: thesis: ex p being Nat st
for n0, m0 being Nat st n0 >= p & m0 >= p holds
||.((s2 . n0) - (s2 . m0)).|| < r
then consider p being Nat such that
A4: for n, m being Nat st p <= n & p <= m holds
dist ((s1 . n),(s1 . m)) < r by A3;
take p = p; :: thesis: for n0, m0 being Nat st n0 >= p & m0 >= p holds
||.((s2 . n0) - (s2 . m0)).|| < r
hereby :: thesis: verum
let n0, m0 be Nat; :: thesis: ( n0 >= p & m0 >= p implies ||.((s2 . n0) - (s2 . m0)).|| < r )
assume A5: ( n0 >= p & m0 >= p ) ; :: thesis: ||.((s2 . n0) - (s2 . m0)).|| < r
dist ((s1 . n0),(s1 . m0)) = ||.((s2 . n0) - (s2 . m0)).|| by A1, Th9;
hence ||.((s2 . n0) - (s2 . m0)).|| < r by A5, A4; :: thesis: verum
end;
end;
hence s2 is Cauchy_sequence_by_Norm by RSSPACE3:8; :: thesis: verum
end;
assume A9: s2 is Cauchy_sequence_by_Norm ; :: thesis: s1 is Cauchy
now :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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 :: thesis: 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; :: thesis: for n0, m0 being Nat st k <= n0 & k <= m0 holds
dist ((s1 . n0),(s1 . m0)) < r
hereby :: thesis: verum
let n0, m0 be Nat; :: thesis: ( k <= n0 & k <= m0 implies dist ((s1 . n0),(s1 . m0)) < r )
assume A11: ( k <= n0 & k <= m0 ) ; :: thesis: dist ((s1 . n0),(s1 . m0)) < r
||.((s2 . n0) - (s2 . m0)).|| = dist ((s1 . n0),(s1 . m0)) by A1, Th9;
hence dist ((s1 . n0),(s1 . m0)) < r by A11, A10; :: thesis: verum
end;
end;
hence ex p being Nat st
for n, m being Nat st p <= n & p <= m holds
dist ((s1 . n),(s1 . m)) < r ; :: thesis: verum
end;
hence s1 is Cauchy ; :: thesis: verum