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))
set s1 = Partial_Sums s;
set s2 = Partial_Sums ||.s.||;
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 n <= m ; :: thesis: ||.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).|| <= abs (((Partial_Sums ||.s.||) . m) - ((Partial_Sums ||.s.||) . n))
then reconsider k = m - n as Element of NAT by INT_1:18;
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));
A1: n + k = m ;

now

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

end;

then A2: Partial_Sums ||.s.|| is non-decreasing by SERIES_1:19;
A3: 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] )
A4: 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 NORMSP_0:def 4
.= abs (||.(s . ((n + k) + 1)).|| + (((Partial_Sums ||.s.||) . (n + k)) - ((Partial_Sums ||.s.||) . n))) ;
||.(((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 A5: ||.(((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 14;
(Partial_Sums ||.s.||) . (n + k) >= (Partial_Sums ||.s.||) . n by A2, SEQM_3:11;
then A6: ((Partial_Sums ||.s.||) . (n + k)) - ((Partial_Sums ||.s.||) . n) >= 0 by XREAL_1:50;
assume ||.(((Partial_Sums s) . (n + k)) - ((Partial_Sums s) . n)).|| <= abs (((Partial_Sums ||.s.||) . (n + k)) - ((Partial_Sums ||.s.||) . n)) ; :: thesis: S₁[k + 1]
then ||.(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 XREAL_1:9;
then ||.(((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 A5, XXREAL_0:2;
then A7: ||.(((Partial_Sums s) . (n + (k + 1))) - ((Partial_Sums s) . n)).|| <= ||.(s . ((n + k) + 1)).|| + (((Partial_Sums ||.s.||) . (n + k)) - ((Partial_Sums ||.s.||) . n)) by A6, ABSVALUE:def 1;
||.(s . ((n + k) + 1)).|| >= 0 by CLVECT_1:106;
hence S₁[k + 1] by A6, A7, A4, ABSVALUE:def 1; :: thesis: verum

end;

||.(((Partial_Sums s) . (n + 0)) - ((Partial_Sums s) . n)).|| = ||.(0. X).|| by RLVECT_1:28
.= 0 ;
then A8: S₁[ 0 ] by COMPLEX1:132;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A8, A3);
hence ||.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).|| <= abs (((Partial_Sums ||.s.||) . m) - ((Partial_Sums ||.s.||) . n)) by A1; :: thesis: verum