let seq be Real_Sequence; :: thesis: for n, m being Element of NAT st m <= n holds
( abs (((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)) <= ((Partial_Sums (abs seq)) . n) - ((Partial_Sums (abs seq)) . m) & abs (((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)) <= (Partial_Sums (abs seq)) . n )
let n, m be Element of NAT ; :: thesis: ( m <= n implies ( abs (((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)) <= ((Partial_Sums (abs seq)) . n) - ((Partial_Sums (abs seq)) . m) & abs (((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)) <= (Partial_Sums (abs seq)) . n ) )
assume A1: m <= n ; :: thesis: ( abs (((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)) <= ((Partial_Sums (abs seq)) . n) - ((Partial_Sums (abs seq)) . m) & abs (((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)) <= (Partial_Sums (abs seq)) . n )
A2: for n being Element of NAT holds (abs seq) . n >= 0

proof

let n be Element of NAT ; :: thesis: (abs seq) . n >= 0
abs (seq . n) = (abs seq) . n by SEQ_1:12;
hence (abs seq) . n >= 0 by COMPLEX1:46; :: thesis: verum

end;

then A3: abs (((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 abs (((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 ( abs (((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)) <= ((Partial_Sums (abs seq)) . n) - ((Partial_Sums (abs seq)) . m) & abs (((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)) <= (Partial_Sums (abs seq)) . n ) by A3, A1, SERIES_1:34; :: thesis: verum