let X be ComplexNormSpace; :: thesis: for s being sequence of X
for n, m being Nat st n <= m holds
||.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).|| <= |.(((Partial_Sums ||.s.||) . m) - ((Partial_Sums ||.s.||) . n)).|
let s be sequence of X; :: thesis: for n, m being Nat st n <= m holds
||.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).|| <= |.(((Partial_Sums ||.s.||) . m) - ((Partial_Sums ||.s.||) . n)).|
set s1 = Partial_Sums s;
set s2 = Partial_Sums ||.s.||;
let n, m be Nat; :: thesis: ( n <= m implies ||.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).|| <= |.(((Partial_Sums ||.s.||) . m) - ((Partial_Sums ||.s.||) . n)).| )
assume n <= m ; :: thesis: ||.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).|| <= |.(((Partial_Sums ||.s.||) . m) - ((Partial_Sums ||.s.||) . n)).|
then reconsider k = m - n as Element of NAT by INT_1:5;
defpred S₁[ Nat] means ||.(((Partial_Sums s) . (n + $1)) - ((Partial_Sums s) . n)).|| <= |.(((Partial_Sums ||.s.||) . (n + $1)) - ((Partial_Sums ||.s.||) . n)).|;
A1: n + k = m ;

now :: thesis: for k being Nat holds ||.s.|| . k >= 0

let k be Nat; :: thesis: ||.s.|| . k >= 0
||.(s . k).|| >= 0 by CLVECT_1:105;
hence ||.s.|| . k >= 0 by NORMSP_0:def 4; :: thesis: verum

end;

then A2: Partial_Sums ||.s.|| is non-decreasing by SERIES_1:16;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
A4: |.(((Partial_Sums ||.s.||) . (n + (k + 1))) - ((Partial_Sums ||.s.||) . n)).| = |.((((Partial_Sums ||.s.||) . (n + k)) + (||.s.|| . ((n + k) + 1))) - ((Partial_Sums ||.s.||) . n)).| by SERIES_1:def 1
.= |.((((Partial_Sums ||.s.||) . (n + k)) + ||.(s . ((n + k) + 1)).||) - ((Partial_Sums ||.s.||) . n)).| by NORMSP_0:def 4
.= |.(||.(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 3 ;
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 13;
(Partial_Sums ||.s.||) . (n + k) >= (Partial_Sums ||.s.||) . n by A2, SEQM_3:5;
then A6: ((Partial_Sums ||.s.||) . (n + k)) - ((Partial_Sums ||.s.||) . n) >= 0 by XREAL_1:48;
assume ||.(((Partial_Sums s) . (n + k)) - ((Partial_Sums s) . n)).|| <= |.(((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)).|| + |.(((Partial_Sums ||.s.||) . (n + k)) - ((Partial_Sums ||.s.||) . n)).| by XREAL_1:7;
then ||.(((Partial_Sums s) . (n + (k + 1))) - ((Partial_Sums s) . n)).|| <= ||.(s . ((n + k) + 1)).|| + |.(((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:105;
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:15
.= 0 ;
then A8: S₁[ 0 ] by COMPLEX1:46;
for k being Nat holds S₁[k] from NAT_1:sch 2(A8, A3);
hence ||.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).|| <= |.(((Partial_Sums ||.s.||) . m) - ((Partial_Sums ||.s.||) . n)).| by A1; :: thesis: verum