let X be RealUnitarySpace; :: thesis: for s1 being sequence of X
for s2 being sequence of (RUSp2RNSp X) st s1 = s2 holds
( s2 is Cauchy_sequence_by_Norm iff s1 is Cauchy )
let s1 be sequence of X; :: thesis: for s2 being sequence of (RUSp2RNSp X) st s1 = s2 holds
( s2 is Cauchy_sequence_by_Norm iff s1 is Cauchy )
let s2 be sequence of (RUSp2RNSp X); :: thesis: ( s1 = s2 implies ( s2 is Cauchy_sequence_by_Norm iff s1 is Cauchy ) )
assume A0: s1 = s2 ; :: thesis: ( s2 is Cauchy_sequence_by_Norm iff s1 is Cauchy )

hereby :: thesis: ( s1 is Cauchy implies s2 is Cauchy_sequence_by_Norm )

assume AS: s2 is Cauchy_sequence_by_Norm ; :: thesis: s1 is Cauchy
for r being Real st 0 < r holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((s1 . n) - (s1 . m)).|| < r

proof

let r be Real; :: thesis: ( 0 < r implies ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((s1 . n) - (s1 . m)).|| < r )
assume 0 < r ; :: thesis: ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((s1 . n) - (s1 . m)).|| < r
then consider k being Nat such that
P1: for n, m being Nat st n >= k & m >= k holds
||.((s2 . n) - (s2 . m)).|| < r by AS, RSSPACE3:8;
take k ; :: thesis: for n, m being Nat st n >= k & m >= k holds
||.((s1 . n) - (s1 . m)).|| < r
thus for n, m being Nat st n >= k & m >= k holds
||.((s1 . n) - (s1 . m)).|| < r :: thesis: verum

proof

let n, m be Nat; :: thesis: ( n >= k & m >= k implies ||.((s1 . n) - (s1 . m)).|| < r )
assume ( n >= k & m >= k ) ; :: thesis: ||.((s1 . n) - (s1 . m)).|| < r
then P2: ||.((s2 . n) - (s2 . m)).|| < r by P1;
(s2 . n) - (s2 . m) = (s1 . n) - (s1 . m) by A0, RHS3;
hence ||.((s1 . n) - (s1 . m)).|| < r by Def1, P2; :: thesis: verum

end;

end;

hence s1 is Cauchy by BHSP_3:2; :: thesis: verum

end;

assume A1: s1 is Cauchy ; :: thesis: s2 is Cauchy_sequence_by_Norm
for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((s2 . n) - (s2 . m)).|| < r

proof

let r be Real; :: thesis: ( r > 0 implies ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((s2 . n) - (s2 . m)).|| < r )
assume r > 0 ; :: thesis: ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((s2 . n) - (s2 . m)).|| < r
then consider k being Nat such that
A2: for n, m being Nat st n >= k & m >= k holds
||.((s1 . n) - (s1 . m)).|| < r by A1, BHSP_3:2;
take k ; :: thesis: for n, m being Nat st n >= k & m >= k holds
||.((s2 . n) - (s2 . m)).|| < r
thus for n, m being Nat st n >= k & m >= k holds
||.((s2 . n) - (s2 . m)).|| < r :: thesis: verum

proof

let n, m be Nat; :: thesis: ( n >= k & m >= k implies ||.((s2 . n) - (s2 . m)).|| < r )
assume ( n >= k & m >= k ) ; :: thesis: ||.((s2 . n) - (s2 . m)).|| < r
then A3: ||.((s1 . n) - (s1 . m)).|| < r by A2;
(s1 . n) - (s1 . m) = (s2 . n) - (s2 . m) by A0, RHS3;
hence ||.((s2 . n) - (s2 . m)).|| < r by Def1, A3; :: thesis: verum

end;

end;

hence s2 is Cauchy_sequence_by_Norm by RSSPACE3:8; :: thesis: verum