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 6;
hence ||.((Sum seq,m) - (Sum seq,n)).|| <= abs ((Sum ||.seq.||,m) - (Sum ||.seq.||,n)) by SERIES_1:def 6; :: thesis: verum