let X be ComplexHilbertSpace; :: thesis: for seq being sequence of X holds
( seq is summable iff for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.(Sum (seq,n,m)).|| < r )
let seq be sequence of X; :: thesis: ( seq is summable iff for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.(Sum (seq,n,m)).|| < r )
thus ( seq is summable implies for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.(Sum (seq,n,m)).|| < r ) :: thesis: ( ( for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.(Sum (seq,n,m)).|| < r ) implies seq is summable )

proof

assume A1: seq is summable ; :: thesis: for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.(Sum (seq,n,m)).|| < r

now :: thesis: for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.(Sum (seq,n,m)).|| < r

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

end;

hence for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.(Sum (seq,n,m)).|| < r ; :: thesis: verum

end;

thus ( ( for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.(Sum (seq,n,m)).|| < r ) implies seq is summable ) :: thesis: verum

proof

assume A3: for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.(Sum (seq,n,m)).|| < r ; :: thesis: seq is summable

now :: thesis: for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((Sum (seq,n)) - (Sum (seq,m))).|| < r

let r be Real; :: thesis: ( r > 0 implies ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((Sum (seq,n)) - (Sum (seq,m))).|| < r )
assume r > 0 ; :: thesis: ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((Sum (seq,n)) - (Sum (seq,m))).|| < r
then consider k being Nat such that
A4: for n, m being Nat st n >= k & m >= k holds
||.(Sum (seq,n,m)).|| < r by A3;
take k = k; :: thesis: for n, m being Nat st n >= k & m >= k holds
||.((Sum (seq,n)) - (Sum (seq,m))).|| < r
let n, m be Nat; :: thesis: ( n >= k & m >= k implies ||.((Sum (seq,n)) - (Sum (seq,m))).|| < r )
assume ( n >= k & m >= k ) ; :: thesis: ||.((Sum (seq,n)) - (Sum (seq,m))).|| < r
then ||.(Sum (seq,n,m)).|| < r by A4;
hence ||.((Sum (seq,n)) - (Sum (seq,m))).|| < r ; :: thesis: verum

end;

hence seq is summable by Th23; :: thesis: verum

end;