let X be RealNormSpace; :: thesis: for seq being sequence of X holds

( seq is Cauchy_sequence_by_Norm iff for p being Real st p > 0 holds

ex n being Nat st

for m being Nat st n <= m holds

||.((seq . m) - (seq . n)).|| < p )

let seq be sequence of X; :: thesis: ( seq is Cauchy_sequence_by_Norm iff for p being Real st p > 0 holds

ex n being Nat st

for m being Nat st n <= m holds

||.((seq . m) - (seq . n)).|| < p )

ex n being Nat st

for m being Nat st n <= m holds

||.((seq . m) - (seq . n)).|| < p ) by A1; :: thesis: verum

( seq is Cauchy_sequence_by_Norm iff for p being Real st p > 0 holds

ex n being Nat st

for m being Nat st n <= m holds

||.((seq . m) - (seq . n)).|| < p )

let seq be sequence of X; :: thesis: ( seq is Cauchy_sequence_by_Norm iff for p being Real st p > 0 holds

ex n being Nat st

for m being Nat st n <= m holds

||.((seq . m) - (seq . n)).|| < p )

A1: now :: thesis: ( ( for p being Real st p > 0 holds

ex n being Nat st

for m being Nat st n <= m holds

||.((seq . m) - (seq . n)).|| < p ) implies seq is Cauchy_sequence_by_Norm )

ex n being Nat st

for m being Nat st n <= m holds

||.((seq . m) - (seq . n)).|| < p ) implies seq is Cauchy_sequence_by_Norm )

assume A2:
for p being Real st p > 0 holds

ex n being Nat st

for m being Nat st n <= m holds

||.((seq . m) - (seq . n)).|| < p ; :: thesis: seq is Cauchy_sequence_by_Norm

end;ex n being Nat st

for m being Nat st n <= m holds

||.((seq . m) - (seq . n)).|| < p ; :: thesis: seq is Cauchy_sequence_by_Norm

now :: thesis: for s being Real st 0 < s holds

ex k being Nat st

for m, n being Nat st k <= m & k <= n holds

||.((seq . m) - (seq . n)).|| < s

hence
seq is Cauchy_sequence_by_Norm
by RSSPACE3:8; :: thesis: verumex k being Nat st

for m, n being Nat st k <= m & k <= n holds

||.((seq . m) - (seq . n)).|| < s

let s be Real; :: thesis: ( 0 < s implies ex k being Nat st

for m, n being Nat st k <= m & k <= n holds

||.((seq . m) - (seq . n)).|| < s )

reconsider ss = s as Real ;

assume 0 < s ; :: thesis: ex k being Nat st

for m, n being Nat st k <= m & k <= n holds

||.((seq . m) - (seq . n)).|| < s

then consider k being Nat such that

A3: for m being Nat st k <= m holds

||.((seq . m) - (seq . k)).|| < ss / 2 by A2, XREAL_1:215;

for m, n being Nat st k <= m & k <= n holds

||.((seq . m) - (seq . n)).|| < s ; :: thesis: verum

end;for m, n being Nat st k <= m & k <= n holds

||.((seq . m) - (seq . n)).|| < s )

reconsider ss = s as Real ;

assume 0 < s ; :: thesis: ex k being Nat st

for m, n being Nat st k <= m & k <= n holds

||.((seq . m) - (seq . n)).|| < s

then consider k being Nat such that

A3: for m being Nat st k <= m holds

||.((seq . m) - (seq . k)).|| < ss / 2 by A2, XREAL_1:215;

now :: thesis: for m, n being Nat st k <= m & k <= n holds

||.((seq . m) - (seq . n)).|| < s

hence
ex k being Nat st ||.((seq . m) - (seq . n)).|| < s

let m, n be Nat; :: thesis: ( k <= m & k <= n implies ||.((seq . m) - (seq . n)).|| < s )

assume that

A4: k <= m and

A5: k <= n ; :: thesis: ||.((seq . m) - (seq . n)).|| < s

||.((seq . n) - (seq . k)).|| < s / 2 by A3, A5;

then A6: ||.((seq . k) - (seq . n)).|| < s / 2 by NORMSP_1:7;

||.((seq . m) - (seq . k)).|| < s / 2 by A3, A4;

then A7: ||.((seq . m) - (seq . k)).|| + ||.((seq . k) - (seq . n)).|| < (s / 2) + (s / 2) by A6, XREAL_1:8;

( ||.(((seq . m) - (seq . k)) + ((seq . k) - (seq . n))).|| <= ||.((seq . m) - (seq . k)).|| + ||.((seq . k) - (seq . n)).|| & ||.(((seq . m) - (seq . k)) + ((seq . k) - (seq . n))).|| = ||.((seq . m) - (seq . n)).|| ) by Th3, NORMSP_1:def 1;

hence ||.((seq . m) - (seq . n)).|| < s by A7, XXREAL_0:2; :: thesis: verum

end;assume that

A4: k <= m and

A5: k <= n ; :: thesis: ||.((seq . m) - (seq . n)).|| < s

||.((seq . n) - (seq . k)).|| < s / 2 by A3, A5;

then A6: ||.((seq . k) - (seq . n)).|| < s / 2 by NORMSP_1:7;

||.((seq . m) - (seq . k)).|| < s / 2 by A3, A4;

then A7: ||.((seq . m) - (seq . k)).|| + ||.((seq . k) - (seq . n)).|| < (s / 2) + (s / 2) by A6, XREAL_1:8;

( ||.(((seq . m) - (seq . k)) + ((seq . k) - (seq . n))).|| <= ||.((seq . m) - (seq . k)).|| + ||.((seq . k) - (seq . n)).|| & ||.(((seq . m) - (seq . k)) + ((seq . k) - (seq . n))).|| = ||.((seq . m) - (seq . n)).|| ) by Th3, NORMSP_1:def 1;

hence ||.((seq . m) - (seq . n)).|| < s by A7, XXREAL_0:2; :: thesis: verum

for m, n being Nat st k <= m & k <= n holds

||.((seq . m) - (seq . n)).|| < s ; :: thesis: verum

now :: thesis: ( seq is Cauchy_sequence_by_Norm implies for p being Real st p > 0 holds

ex n being Nat st

for m being Nat st n <= m holds

||.((seq . m) - (seq . n)).|| < p )

hence
( seq is Cauchy_sequence_by_Norm iff for p being Real st p > 0 holds ex n being Nat st

for m being Nat st n <= m holds

||.((seq . m) - (seq . n)).|| < p )

assume A8:
seq is Cauchy_sequence_by_Norm
; :: thesis: for p being Real st p > 0 holds

ex n being Nat st

for m being Nat st n <= m holds

||.((seq . m) - (seq . n)).|| < p

thus for p being Real st p > 0 holds

ex n being Nat st

for m being Nat st n <= m holds

||.((seq . m) - (seq . n)).|| < p :: thesis: verum

end;ex n being Nat st

for m being Nat st n <= m holds

||.((seq . m) - (seq . n)).|| < p

thus for p being Real st p > 0 holds

ex n being Nat st

for m being Nat st n <= m holds

||.((seq . m) - (seq . n)).|| < p :: thesis: verum

proof

let p be Real; :: thesis: ( p > 0 implies ex n being Nat st

for m being Nat st n <= m holds

||.((seq . m) - (seq . n)).|| < p )

assume p > 0 ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

||.((seq . m) - (seq . n)).|| < p

then consider n being Nat such that

A9: for m, k being Nat st n <= m & n <= k holds

||.((seq . m) - (seq . k)).|| < p by A8, RSSPACE3:8;

for m being Nat st n <= m holds

||.((seq . m) - (seq . n)).|| < p by A9;

hence ex n being Nat st

for m being Nat st n <= m holds

||.((seq . m) - (seq . n)).|| < p ; :: thesis: verum

end;for m being Nat st n <= m holds

||.((seq . m) - (seq . n)).|| < p )

assume p > 0 ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

||.((seq . m) - (seq . n)).|| < p

then consider n being Nat such that

A9: for m, k being Nat st n <= m & n <= k holds

||.((seq . m) - (seq . k)).|| < p by A8, RSSPACE3:8;

for m being Nat st n <= m holds

||.((seq . m) - (seq . n)).|| < p by A9;

hence ex n being Nat st

for m being Nat st n <= m holds

||.((seq . m) - (seq . n)).|| < p ; :: thesis: verum

ex n being Nat st

for m being Nat st n <= m holds

||.((seq . m) - (seq . n)).|| < p ) by A1; :: thesis: verum