let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X
for n, m being Nat holds ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= |.(((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)).|
let seq be sequence of X; :: thesis: for n, m being Nat holds ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= |.(((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)).|
let n, m be Nat; :: thesis: ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= |.(((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)).|

A1: now :: thesis: ( n >= m implies ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= |.(((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)).| )

reconsider d = n, t = m as Integer ;
set PSseq9 = Partial_Sums ||.seq.||;
set PSseq = Partial_Sums seq;
defpred S₁[ Nat] means ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + $1))).|| <= |.(((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . (m + $1))).|;
A2: Partial_Sums ||.seq.|| is non-decreasing by Th35;

A3: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
A4: ||.(seq . ((m + k) + 1)).|| >= 0 by CSSPACE:44;
A5: |.(((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . (m + (k + 1)))).| = |.(- (((Partial_Sums ||.seq.||) . (m + (k + 1))) - ((Partial_Sums ||.seq.||) . m))).|
.= |.(((Partial_Sums ||.seq.||) . ((m + k) + 1)) - ((Partial_Sums ||.seq.||) . m)).| by COMPLEX1:52
.= |.((((Partial_Sums ||.seq.||) . (m + k)) + (||.seq.|| . ((m + k) + 1))) - ((Partial_Sums ||.seq.||) . m)).| by SERIES_1:def 1
.= |.((||.(seq . ((m + k) + 1)).|| + ((Partial_Sums ||.seq.||) . (m + k))) - ((Partial_Sums ||.seq.||) . m)).| by CLVECT_2:def 3
.= |.((((Partial_Sums ||.seq.||) . (m + k)) - ((Partial_Sums ||.seq.||) . m)) + ||.(seq . ((m + k) + 1)).||).| ;
||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + (k + 1)))).|| = ||.(((Partial_Sums seq) . m) - (((Partial_Sums seq) . (m + k)) + (seq . ((m + k) + 1)))).|| by BHSP_4:def 1
.= ||.((((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + k))) - (seq . ((m + k) + 1))).|| by RLVECT_1:27
.= ||.((((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + k))) + (- (seq . ((m + k) + 1)))).|| ;
then ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + (k + 1)))).|| <= ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + k))).|| + ||.(- (seq . ((m + k) + 1))).|| by CSSPACE:46;
then A6: ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + (k + 1)))).|| <= ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + k))).|| + ||.(seq . ((m + k) + 1)).|| by CSSPACE:47;
(Partial_Sums ||.seq.||) . (m + k) >= (Partial_Sums ||.seq.||) . m by A2, SEQM_3:5;
then A7: ((Partial_Sums ||.seq.||) . (m + k)) - ((Partial_Sums ||.seq.||) . m) >= 0 by XREAL_1:48;
assume S₁[k] ; :: thesis: S₁[k + 1]
then ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + k))).|| + ||.(seq . ((m + k) + 1)).|| <= |.(((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . (m + k))).| + ||.(seq . ((m + k) + 1)).|| by XREAL_1:6;
then ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + (k + 1)))).|| <= |.(- (((Partial_Sums ||.seq.||) . (m + k)) - ((Partial_Sums ||.seq.||) . m))).| + ||.(seq . ((m + k) + 1)).|| by A6, XXREAL_0:2;
then ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + (k + 1)))).|| <= |.(((Partial_Sums ||.seq.||) . (m + k)) - ((Partial_Sums ||.seq.||) . m)).| + ||.(seq . ((m + k) + 1)).|| by COMPLEX1:52;
then ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + (k + 1)))).|| <= (((Partial_Sums ||.seq.||) . (m + k)) - ((Partial_Sums ||.seq.||) . m)) + ||.(seq . ((m + k) + 1)).|| by A7, ABSVALUE:def 1;
hence S₁[k + 1] by A7, A4, A5, ABSVALUE:def 1; :: thesis: verum

end;

assume n >= m ; :: thesis: ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= |.(((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)).|
then reconsider k = d - t as Element of NAT by INT_1:5;
A8: m + k = n ;
||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + 0))).|| = ||.H₁(X).|| by RLVECT_1:15
.= 0 by CSSPACE:42 ;
then A9: S₁[ 0 ] by COMPLEX1:46;
for k being Nat holds S₁[k] from NAT_1:sch 2(A9, A3);
hence ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= |.(((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)).| by A8; :: thesis: verum

end;

now :: thesis: ( n <= m implies ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= |.(((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)).| )

reconsider d = n, t = m as Integer ;
set PSseq9 = Partial_Sums ||.seq.||;
set PSseq = Partial_Sums seq;
defpred S₁[ Nat] means ||.(((Partial_Sums seq) . (n + $1)) - ((Partial_Sums seq) . n)).|| <= |.(((Partial_Sums ||.seq.||) . (n + $1)) - ((Partial_Sums ||.seq.||) . n)).|;
A10: Partial_Sums ||.seq.|| is non-decreasing by Th35;

A11: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
A12: |.(((Partial_Sums ||.seq.||) . (n + (k + 1))) - ((Partial_Sums ||.seq.||) . n)).| = |.((((Partial_Sums ||.seq.||) . (n + k)) + (||.seq.|| . ((n + k) + 1))) - ((Partial_Sums ||.seq.||) . n)).| by SERIES_1:def 1
.= |.((||.(seq . ((n + k) + 1)).|| + ((Partial_Sums ||.seq.||) . (n + k))) - ((Partial_Sums ||.seq.||) . n)).| by CLVECT_2:def 3
.= |.(||.(seq . ((n + k) + 1)).|| + (((Partial_Sums ||.seq.||) . (n + k)) - ((Partial_Sums ||.seq.||) . n))).| ;
||.(((Partial_Sums seq) . (n + (k + 1))) - ((Partial_Sums seq) . n)).|| = ||.(((seq . ((n + k) + 1)) + ((Partial_Sums seq) . (n + k))) - ((Partial_Sums seq) . n)).|| by BHSP_4:def 1
.= ||.((seq . ((n + k) + 1)) + (((Partial_Sums seq) . (n + k)) - ((Partial_Sums seq) . n))).|| by RLVECT_1:def 3 ;
then A13: ||.(((Partial_Sums seq) . (n + (k + 1))) - ((Partial_Sums seq) . n)).|| <= ||.(seq . ((n + k) + 1)).|| + ||.(((Partial_Sums seq) . (n + k)) - ((Partial_Sums seq) . n)).|| by CSSPACE:46;
(Partial_Sums ||.seq.||) . (n + k) >= (Partial_Sums ||.seq.||) . n by A10, SEQM_3:5;
then A14: ((Partial_Sums ||.seq.||) . (n + k)) - ((Partial_Sums ||.seq.||) . n) >= 0 by XREAL_1:48;
assume S₁[k] ; :: thesis: S₁[k + 1]
then ||.(seq . ((n + k) + 1)).|| + ||.(((Partial_Sums seq) . (n + k)) - ((Partial_Sums seq) . n)).|| <= ||.(seq . ((n + k) + 1)).|| + |.(((Partial_Sums ||.seq.||) . (n + k)) - ((Partial_Sums ||.seq.||) . n)).| by XREAL_1:7;
then ||.(((Partial_Sums seq) . (n + (k + 1))) - ((Partial_Sums seq) . n)).|| <= ||.(seq . ((n + k) + 1)).|| + |.(((Partial_Sums ||.seq.||) . (n + k)) - ((Partial_Sums ||.seq.||) . n)).| by A13, XXREAL_0:2;
then A15: ||.(((Partial_Sums seq) . (n + (k + 1))) - ((Partial_Sums seq) . n)).|| <= ||.(seq . ((n + k) + 1)).|| + (((Partial_Sums ||.seq.||) . (n + k)) - ((Partial_Sums ||.seq.||) . n)) by A14, ABSVALUE:def 1;
||.(seq . ((n + k) + 1)).|| >= 0 by CSSPACE:44;
hence S₁[k + 1] by A14, A15, A12, ABSVALUE:def 1; :: thesis: verum

end;

assume n <= m ; :: thesis: ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= |.(((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)).|
then reconsider k = t - d as Element of NAT by INT_1:5;
A16: n + k = m ;
||.(((Partial_Sums seq) . (n + 0)) - ((Partial_Sums seq) . n)).|| = ||.H₁(X).|| by RLVECT_1:15
.= 0 by CSSPACE:42 ;
then A17: S₁[ 0 ] by COMPLEX1:46;
for k being Nat holds S₁[k] from NAT_1:sch 2(A17, A11);
hence ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= |.(((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)).| by A16; :: thesis: verum

end;

hence ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= |.(((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)).| by A1; :: thesis: verum