let X be RealNormSpace; :: thesis: for seq being sequence of X holds
( seq is CCauchy iff for p being Real st p > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (seq . n)).|| < p )
let seq be sequence of X; :: thesis: ( seq is CCauchy iff for p being Real st p > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (seq . n)).|| < p )

A1: now

assume A2: for p being Real st p > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (seq . n)).|| < p ; :: thesis: seq is CCauchy

now

let s be Real; :: thesis: ( 0 < s implies ex k being Element of NAT st
for m, n being Element of NAT st k <= m & k <= n holds
||.((seq . m) - (seq . n)).|| < s )
assume 0 < s ; :: thesis: ex k being Element of NAT st
for m, n being Element of NAT st k <= m & k <= n holds
||.((seq . m) - (seq . n)).|| < s
then consider k being Element of NAT such that
A3: for m being Element of NAT st k <= m holds
||.((seq . m) - (seq . k)).|| < s / 2 by A2, XREAL_1:215;

now

let m, n be Element of 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;

hence ex k being Element of NAT st
for m, n being Element of NAT st k <= m & k <= n holds
||.((seq . m) - (seq . n)).|| < s ; :: thesis: verum

end;

hence seq is CCauchy by RSSPACE3:8; :: thesis: verum

end;

now

assume A8: seq is CCauchy ; :: thesis: for p being Real st p > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (seq . n)).|| < p
thus for p being Real st p > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (seq . n)).|| < p :: thesis: verum

proof

let p be Real; :: thesis: ( p > 0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (seq . n)).|| < p )
assume p > 0 ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (seq . n)).|| < p
then consider n being Element of NAT such that
A9: for m, k being Element of NAT st n <= m & n <= k holds
||.((seq . m) - (seq . k)).|| < p by A8, RSSPACE3:8;
for m being Element of NAT st n <= m holds
||.((seq . m) - (seq . n)).|| < p by A9;
hence ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (seq . n)).|| < p ; :: thesis: verum

end;

end;

hence ( seq is CCauchy iff for p being Real st p > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (seq . n)).|| < p ) by A1; :: thesis: verum