let seq be Complex_Sequence; :: thesis: Partial_Sums |.seq.| is non-decreasing
for n being Nat holds 0 <= |.seq.| . n by Lm3;
hence Partial_Sums |.seq.| is non-decreasing by SERIES_1:16; :: thesis: verum