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