let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X
for n, m being Nat holds ||.((Sum (seq,m)) - (Sum (seq,n))).|| <= |.((Sum (||.seq.||,m)) - (Sum (||.seq.||,n))).|
let seq be sequence of X; :: thesis: for n, m being Nat holds ||.((Sum (seq,m)) - (Sum (seq,n))).|| <= |.((Sum (||.seq.||,m)) - (Sum (||.seq.||,n))).|
let n, m be Nat; :: thesis: ||.((Sum (seq,m)) - (Sum (seq,n))).|| <= |.((Sum (||.seq.||,m)) - (Sum (||.seq.||,n))).|
||.((Sum (seq,m)) - ((Partial_Sums seq) . n)).|| <= |.(((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)).| by Th39;
then ||.((Sum (seq,m)) - (Sum (seq,n))).|| <= |.((Sum (||.seq.||,m)) - ((Partial_Sums ||.seq.||) . n)).| by SERIES_1:def 5;
hence ||.((Sum (seq,m)) - (Sum (seq,n))).|| <= |.((Sum (||.seq.||,m)) - (Sum (||.seq.||,n))).| by SERIES_1:def 5; :: thesis: verum