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

for s being Real st 0 < s holds

ex n being Nat st

for m being Nat st n <= m holds

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

let seq be sequence of X; :: thesis: ( seq is convergent implies for s being Real st 0 < s holds

ex n being Nat st

for m being Nat st n <= m holds

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

assume seq is convergent ; :: thesis: for s being Real st 0 < s holds

ex n being Nat st

for m being Nat st n <= m holds

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

then consider g1 being Element of X such that

A1: for s being Real st 0 < s holds

ex n being Nat st

for m being Nat st n <= m holds

||.((seq . m) - g1).|| < s ;

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

for m being Nat st n <= m holds

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

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

for m being Nat st n <= m holds

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

then consider n being Nat such that

A2: for m being Nat st n <= m holds

||.((seq . m) - g1).|| < s / 2 by A1, XREAL_1:215;

for m being Nat st n <= m holds

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

for s being Real st 0 < s holds

ex n being Nat st

for m being Nat st n <= m holds

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

let seq be sequence of X; :: thesis: ( seq is convergent implies for s being Real st 0 < s holds

ex n being Nat st

for m being Nat st n <= m holds

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

assume seq is convergent ; :: thesis: for s being Real st 0 < s holds

ex n being Nat st

for m being Nat st n <= m holds

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

then consider g1 being Element of X such that

A1: for s being Real st 0 < s holds

ex n being Nat st

for m being Nat st n <= m holds

||.((seq . m) - g1).|| < s ;

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

for m being Nat st n <= m holds

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

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

for m being Nat st n <= m holds

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

then consider n being Nat such that

A2: for m being Nat st n <= m holds

||.((seq . m) - g1).|| < s / 2 by A1, XREAL_1:215;

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

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

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

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

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

then A3: ||.((seq . m) - g1).|| < s / 2 by A2;

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

||.((seq . n) - g1).|| < s / 2 by A2;

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

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

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

end;assume n <= m ; :: thesis: ||.((seq . m) - (seq . n)).|| < s

then A3: ||.((seq . m) - g1).|| < s / 2 by A2;

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

||.((seq . n) - g1).|| < s / 2 by A2;

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

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

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

for m being Nat st n <= m holds

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