let X be RealUnitarySpace; :: thesis: for seq being sequence of X st X is Hilbert holds
( seq is summable iff for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((Sum seq,n) - (Sum seq,m)).|| < r )
let seq be sequence of X; :: thesis: ( X is Hilbert implies ( seq is summable iff for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((Sum seq,n) - (Sum seq,m)).|| < r ) )
assume A1: X is Hilbert ; :: thesis: ( seq is summable iff for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((Sum seq,n) - (Sum seq,m)).|| < r )
thus ( seq is summable implies for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((Sum seq,n) - (Sum seq,m)).|| < r ) :: thesis: ( ( for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((Sum seq,n) - (Sum seq,m)).|| < r ) implies seq is summable )

proof

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

now

let r be Real; :: thesis: ( r > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((Sum seq,n) - (Sum seq,m)).|| < r )
assume r > 0 ; :: thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((Sum seq,n) - (Sum seq,m)).|| < r
then consider k being Element of NAT such that
A3: for n, m being Element of NAT st n >= k & m >= k holds
||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r by A1, A2, Th10;
take k = k; :: thesis: for n, m being Element of NAT st n >= k & m >= k holds
||.((Sum seq,n) - (Sum seq,m)).|| < r
let n, m be Element of 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
hence ||.((Sum seq,n) - (Sum seq,m)).|| < r by A3; :: thesis: verum

end;

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

end;

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

proof

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

now

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

end;

hence seq is summable by A1, Th10; :: thesis: verum

end;