let seq be Real_Sequence; :: thesis: for n, m being Nat st m <= n holds
( |.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).| <= ((Partial_Sums (abs seq)) . n) - ((Partial_Sums (abs seq)) . m) & |.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).| <= (Partial_Sums (abs seq)) . n )
let n, m be Nat; :: thesis: ( m <= n implies ( |.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).| <= ((Partial_Sums (abs seq)) . n) - ((Partial_Sums (abs seq)) . m) & |.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).| <= (Partial_Sums (abs seq)) . n ) )
assume A1: m <= n ; :: thesis: ( |.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).| <= ((Partial_Sums (abs seq)) . n) - ((Partial_Sums (abs seq)) . m) & |.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).| <= (Partial_Sums (abs seq)) . n )
A2: for n being Nat holds (abs seq) . n >= 0
proof
let n be Nat; :: thesis: (abs seq) . n >= 0
|.(seq . n).| = (abs seq) . n by SEQ_1:12;
hence (abs seq) . n >= 0 by COMPLEX1:46; :: thesis: verum
end;
then A3: |.(((Partial_Sums (abs seq)) . n) - ((Partial_Sums (abs seq)) . m)).| = ((Partial_Sums (abs seq)) . n) - ((Partial_Sums (abs seq)) . m) by A1, COMSEQ_3:9;
(Partial_Sums (abs seq)) . m >= 0 by A2, SERIES_3:34;
then |.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).| <= (((Partial_Sums (abs seq)) . n) - ((Partial_Sums (abs seq)) . m)) + ((Partial_Sums (abs seq)) . m) by A3, A1, SERIES_1:34, XREAL_1:38;
hence ( |.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).| <= ((Partial_Sums (abs seq)) . n) - ((Partial_Sums (abs seq)) . m) & |.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).| <= (Partial_Sums (abs seq)) . n ) by A3, A1, SERIES_1:34; :: thesis: verum