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

A1: now

assume A2: n <= m ; :: thesis: ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n))
set PSseq = Partial_Sums seq;
set PSseq' = Partial_Sums ||.seq.||;
defpred S₁[ Element of NAT ] means ||.(((Partial_Sums seq) . (n + $1)) - ((Partial_Sums seq) . n)).|| <= abs (((Partial_Sums ||.seq.||) . (n + $1)) - ((Partial_Sums ||.seq.||) . n));
||.(((Partial_Sums seq) . (n + 0 )) - ((Partial_Sums seq) . n)).|| = ||.H₁(X).|| by RLVECT_1:28
.= 0 by CSSPACE:44 ;
then A3: S₁[ 0 ] by COMPLEX1:132;
A4: Partial_Sums ||.seq.|| is non-decreasing by Th35;

A5: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]
||.(((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 6 ;
then A7: ||.(((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:48;
||.(seq . ((n + k) + 1)).|| + ||.(((Partial_Sums seq) . (n + k)) - ((Partial_Sums seq) . n)).|| <= ||.(seq . ((n + k) + 1)).|| + (abs (((Partial_Sums ||.seq.||) . (n + k)) - ((Partial_Sums ||.seq.||) . n))) by A6, XREAL_1:9;
then A8: ||.(((Partial_Sums seq) . (n + (k + 1))) - ((Partial_Sums seq) . n)).|| <= ||.(seq . ((n + k) + 1)).|| + (abs (((Partial_Sums ||.seq.||) . (n + k)) - ((Partial_Sums ||.seq.||) . n))) by A7, XXREAL_0:2;
(Partial_Sums ||.seq.||) . (n + k) >= (Partial_Sums ||.seq.||) . n by A4, SEQM_3:11;
then A9: ((Partial_Sums ||.seq.||) . (n + k)) - ((Partial_Sums ||.seq.||) . n) >= 0 by XREAL_1:50;
then A10: ||.(((Partial_Sums seq) . (n + (k + 1))) - ((Partial_Sums seq) . n)).|| <= ||.(seq . ((n + k) + 1)).|| + (((Partial_Sums ||.seq.||) . (n + k)) - ((Partial_Sums ||.seq.||) . n)) by A8, ABSVALUE:def 1;
||.(seq . ((n + k) + 1)).|| >= 0 by CSSPACE:46;
then A11: ||.(seq . ((n + k) + 1)).|| + (((Partial_Sums ||.seq.||) . (n + k)) - ((Partial_Sums ||.seq.||) . n)) >= 0 + 0 by A9;
abs (((Partial_Sums ||.seq.||) . (n + (k + 1))) - ((Partial_Sums ||.seq.||) . n)) = abs ((((Partial_Sums ||.seq.||) . (n + k)) + (||.seq.|| . ((n + k) + 1))) - ((Partial_Sums ||.seq.||) . n)) by SERIES_1:def 1
.= abs ((||.(seq . ((n + k) + 1)).|| + ((Partial_Sums ||.seq.||) . (n + k))) - ((Partial_Sums ||.seq.||) . n)) by CLVECT_2:def 3
.= abs (||.(seq . ((n + k) + 1)).|| + (((Partial_Sums ||.seq.||) . (n + k)) - ((Partial_Sums ||.seq.||) . n))) ;
hence S₁[k + 1] by A10, A11, ABSVALUE:def 1; :: thesis: verum

end;

A12: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A3, A5);
reconsider d = n, t = m as Integer ;
reconsider k = t - d as Element of NAT by A2, INT_1:18;
n + k = m ;
hence ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)) by A12; :: thesis: verum

end;

now

assume A13: n >= m ; :: thesis: ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n))
set PSseq = Partial_Sums seq;
set PSseq' = Partial_Sums ||.seq.||;
defpred S₁[ Element of NAT ] means ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + $1))).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . (m + $1)));
||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + 0 ))).|| = ||.H₁(X).|| by RLVECT_1:28
.= 0 by CSSPACE:44 ;
then A14: S₁[ 0 ] by COMPLEX1:132;
A15: Partial_Sums ||.seq.|| is non-decreasing by Th35;

A16: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A17: S₁[k] ; :: thesis: S₁[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:41
.= ||.((((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:48;
then A18: ||.(((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:49;
||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + k))).|| + ||.(seq . ((m + k) + 1)).|| <= (abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . (m + k)))) + ||.(seq . ((m + k) + 1)).|| by A17, XREAL_1:8;
then ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + (k + 1)))).|| <= (abs (- (((Partial_Sums ||.seq.||) . (m + k)) - ((Partial_Sums ||.seq.||) . m)))) + ||.(seq . ((m + k) + 1)).|| by A18, XXREAL_0:2;
then A19: ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + (k + 1)))).|| <= (abs (((Partial_Sums ||.seq.||) . (m + k)) - ((Partial_Sums ||.seq.||) . m))) + ||.(seq . ((m + k) + 1)).|| by COMPLEX1:138;
(Partial_Sums ||.seq.||) . (m + k) >= (Partial_Sums ||.seq.||) . m by A15, SEQM_3:11;
then A20: ((Partial_Sums ||.seq.||) . (m + k)) - ((Partial_Sums ||.seq.||) . m) >= 0 by XREAL_1:50;
then A21: ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + (k + 1)))).|| <= (((Partial_Sums ||.seq.||) . (m + k)) - ((Partial_Sums ||.seq.||) . m)) + ||.(seq . ((m + k) + 1)).|| by A19, ABSVALUE:def 1;
||.(seq . ((m + k) + 1)).|| >= 0 by CSSPACE:46;
then A22: (((Partial_Sums ||.seq.||) . (m + k)) - ((Partial_Sums ||.seq.||) . m)) + ||.(seq . ((m + k) + 1)).|| >= 0 + 0 by A20;
abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . (m + (k + 1)))) = abs (- (((Partial_Sums ||.seq.||) . (m + (k + 1))) - ((Partial_Sums ||.seq.||) . m)))
.= abs (((Partial_Sums ||.seq.||) . ((m + k) + 1)) - ((Partial_Sums ||.seq.||) . m)) by COMPLEX1:138
.= abs ((((Partial_Sums ||.seq.||) . (m + k)) + (||.seq.|| . ((m + k) + 1))) - ((Partial_Sums ||.seq.||) . m)) by SERIES_1:def 1
.= abs ((||.(seq . ((m + k) + 1)).|| + ((Partial_Sums ||.seq.||) . (m + k))) - ((Partial_Sums ||.seq.||) . m)) by CLVECT_2:def 3
.= abs ((((Partial_Sums ||.seq.||) . (m + k)) - ((Partial_Sums ||.seq.||) . m)) + ||.(seq . ((m + k) + 1)).||) ;
hence S₁[k + 1] by A21, A22, ABSVALUE:def 1; :: thesis: verum

end;

A23: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A14, A16);
reconsider d = n, t = m as Integer ;
reconsider k = d - t as Element of NAT by A13, INT_1:18;
m + k = n ;
hence ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)) by A23; :: thesis: verum

end;

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