let X be ComplexNormSpace; :: thesis: for s being sequence of X
for n, m being Element of NAT st n <= m holds
||.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).|| <= abs (((Partial_Sums ||.s.||) . m) - ((Partial_Sums ||.s.||) . n))
let s be sequence of X; :: thesis: for n, m being Element of NAT st n <= m holds
||.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).|| <= abs (((Partial_Sums ||.s.||) . m) - ((Partial_Sums ||.s.||) . n))
let n, m be Element of NAT ; :: thesis: ( n <= m implies ||.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).|| <= abs (((Partial_Sums ||.s.||) . m) - ((Partial_Sums ||.s.||) . n)) )
assume A1: n <= m ; :: thesis: ||.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).|| <= abs (((Partial_Sums ||.s.||) . m) - ((Partial_Sums ||.s.||) . n))
set s1 = Partial_Sums s;
set s2 = Partial_Sums ||.s.||;
defpred S₁[ Element of NAT ] means ||.(((Partial_Sums s) . (n + $1)) - ((Partial_Sums s) . n)).|| <= abs (((Partial_Sums ||.s.||) . (n + $1)) - ((Partial_Sums ||.s.||) . n));
||.(((Partial_Sums s) . (n + 0 )) - ((Partial_Sums s) . n)).|| = ||.(0. X).|| by RLVECT_1:28
.= 0 by CLVECT_1:103 ;
then A2: S₁[ 0 ] by COMPLEX1:132;

now

let k be Element of NAT ; :: thesis: ||.s.|| . k >= 0
||.(s . k).|| >= 0 by CLVECT_1:106;
hence ||.s.|| . k >= 0 by CLVECT_1:def 17; :: thesis: verum

end;

then A3: Partial_Sums ||.s.|| is non-decreasing by SERIES_1:19;
A4: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: ||.(((Partial_Sums s) . (n + k)) - ((Partial_Sums s) . n)).|| <= abs (((Partial_Sums ||.s.||) . (n + k)) - ((Partial_Sums ||.s.||) . n)) ; :: thesis: S₁[k + 1]
||.(((Partial_Sums s) . (n + (k + 1))) - ((Partial_Sums s) . n)).|| = ||.(((s . ((n + k) + 1)) + ((Partial_Sums s) . (n + k))) - ((Partial_Sums s) . n)).|| by BHSP_4:def 1
.= ||.((s . ((n + k) + 1)) + (((Partial_Sums s) . (n + k)) - ((Partial_Sums s) . n))).|| by RLVECT_1:def 6 ;
then A6: ||.(((Partial_Sums s) . (n + (k + 1))) - ((Partial_Sums s) . n)).|| <= ||.(s . ((n + k) + 1)).|| + ||.(((Partial_Sums s) . (n + k)) - ((Partial_Sums s) . n)).|| by CLVECT_1:def 11;
||.(s . ((n + k) + 1)).|| + ||.(((Partial_Sums s) . (n + k)) - ((Partial_Sums s) . n)).|| <= ||.(s . ((n + k) + 1)).|| + (abs (((Partial_Sums ||.s.||) . (n + k)) - ((Partial_Sums ||.s.||) . n))) by A5, XREAL_1:9;
then A7: ||.(((Partial_Sums s) . (n + (k + 1))) - ((Partial_Sums s) . n)).|| <= ||.(s . ((n + k) + 1)).|| + (abs (((Partial_Sums ||.s.||) . (n + k)) - ((Partial_Sums ||.s.||) . n))) by A6, XXREAL_0:2;
(Partial_Sums ||.s.||) . (n + k) >= (Partial_Sums ||.s.||) . n by A3, SEQM_3:11;
then A8: ((Partial_Sums ||.s.||) . (n + k)) - ((Partial_Sums ||.s.||) . n) >= 0 by XREAL_1:50;
then A9: ||.(((Partial_Sums s) . (n + (k + 1))) - ((Partial_Sums s) . n)).|| <= ||.(s . ((n + k) + 1)).|| + (((Partial_Sums ||.s.||) . (n + k)) - ((Partial_Sums ||.s.||) . n)) by A7, ABSVALUE:def 1;
||.(s . ((n + k) + 1)).|| >= 0 by CLVECT_1:106;
then A10: ||.(s . ((n + k) + 1)).|| + (((Partial_Sums ||.s.||) . (n + k)) - ((Partial_Sums ||.s.||) . n)) >= 0 + 0 by A8;
abs (((Partial_Sums ||.s.||) . (n + (k + 1))) - ((Partial_Sums ||.s.||) . n)) = abs ((((Partial_Sums ||.s.||) . (n + k)) + (||.s.|| . ((n + k) + 1))) - ((Partial_Sums ||.s.||) . n)) by SERIES_1:def 1
.= abs ((((Partial_Sums ||.s.||) . (n + k)) + ||.(s . ((n + k) + 1)).||) - ((Partial_Sums ||.s.||) . n)) by CLVECT_1:def 17
.= abs (||.(s . ((n + k) + 1)).|| + (((Partial_Sums ||.s.||) . (n + k)) - ((Partial_Sums ||.s.||) . n))) ;
hence S₁[k + 1] by A9, A10, ABSVALUE:def 1; :: thesis: verum

end;

A11: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A2, A4);
reconsider k = m - n as Element of NAT by A1, INT_1:18;
n + k = m ;
hence ||.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).|| <= abs (((Partial_Sums ||.s.||) . m) - ((Partial_Sums ||.s.||) . n)) by A11; :: thesis: verum