let X be RealUnitarySpace; :: 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

reconsider d = n, t = m as Integer ;
set PSseq9 = 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)));
A2: Partial_Sums ||.seq.|| is non-decreasing by Th37;

A3: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
A4: ||.(seq . ((m + k) + 1)).|| >= 0 by BHSP_1:34;
A5: 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 BHSP_2:def 3
.= abs ((((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 Def1
.= ||.((((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 BHSP_1:36;
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 BHSP_1:37;
(Partial_Sums ||.seq.||) . (m + k) >= (Partial_Sums ||.seq.||) . m by A2, SEQM_3:11;
then A7: ((Partial_Sums ||.seq.||) . (m + k)) - ((Partial_Sums ||.seq.||) . m) >= 0 by XREAL_1:50;
assume S₁[k] ; :: thesis: S₁[k + 1]
then ||.(((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 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 A6, XXREAL_0:2;
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 COMPLEX1:138;
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)).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n))
then reconsider k = d - t as Element of NAT by INT_1:18;
A8: m + k = n ;
||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . (m + 0))).|| = ||.H₁(X).|| by RLVECT_1:28
.= 0 by BHSP_1:32 ;
then A9: S₁[ 0 ] by COMPLEX1:132;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A9, A3);
hence ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)) by A8; :: thesis: verum

end;

now

reconsider d = n, t = m as Integer ;
set PSseq9 = 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));
A10: Partial_Sums ||.seq.|| is non-decreasing by Th37;

A11: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
A12: ||.(seq . ((n + k) + 1)).|| >= 0 by BHSP_1:34;
A13: 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 BHSP_2:def 3
.= abs (||.(seq . ((n + k) + 1)).|| + (((Partial_Sums ||.seq.||) . (n + k)) - ((Partial_Sums ||.seq.||) . n))) ;
assume S₁[k] ; :: thesis: S₁[k + 1]
then A14: ||.(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 XREAL_1:9;
(Partial_Sums ||.seq.||) . (n + k) >= (Partial_Sums ||.seq.||) . n by A10, SEQM_3:11;
then A15: ((Partial_Sums ||.seq.||) . (n + k)) - ((Partial_Sums ||.seq.||) . n) >= 0 by XREAL_1:50;
||.(((Partial_Sums seq) . (n + (k + 1))) - ((Partial_Sums seq) . n)).|| = ||.(((seq . ((n + k) + 1)) + ((Partial_Sums seq) . (n + k))) - ((Partial_Sums seq) . n)).|| by Def1
.= ||.((seq . ((n + k) + 1)) + (((Partial_Sums seq) . (n + k)) - ((Partial_Sums seq) . n))).|| by RLVECT_1:def 6 ;
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 BHSP_1:36;
then ||.(((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 A14, XXREAL_0:2;
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 A15, ABSVALUE:def 1;
hence S₁[k + 1] by A15, A12, A13, ABSVALUE:def 1; :: thesis: verum

end;

assume n <= m ; :: thesis: ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n))
then reconsider k = t - d as Element of NAT by INT_1:18;
A16: n + k = m ;
||.(((Partial_Sums seq) . (n + 0)) - ((Partial_Sums seq) . n)).|| = ||.H₁(X).|| by RLVECT_1:28
.= 0 by BHSP_1:32 ;
then A17: S₁[ 0 ] by COMPLEX1:132;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A17, A11);
hence ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)) by A16; :: 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