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 AS: 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 )
A3: 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:16;
hence (abs seq) . n >= 0 by COMPLEX1:132; :: thesis: verum

end;

then A4: abs (((Partial_Sums (abs seq)) . n) - ((Partial_Sums (abs seq)) . m)) = ((Partial_Sums (abs seq)) . n) - ((Partial_Sums (abs seq)) . m) by AS, COMSEQ_3:9;
(Partial_Sums (abs seq)) . m >= 0 by A3, 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 A4, AS, SERIES_1:39, XREAL_1:40;
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 A4, AS, SERIES_1:39; :: thesis: verum