let seq be Complex_Sequence; :: thesis: for k being Nat holds |.((Partial_Sums seq) . k).| <= (Partial_Sums |.seq.|) . k
let k be Nat; :: thesis: |.((Partial_Sums seq) . k).| <= (Partial_Sums |.seq.|) . k
defpred S1[ Nat] means |.((Partial_Sums seq) . $1).| <= (Partial_Sums |.seq.|) . $1;
A1: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume S1[k] ; :: thesis: S1[k + 1]
then A2: |.((Partial_Sums seq) . k).| + |.(seq . (k + 1)).| <= ((Partial_Sums |.seq.|) . k) + |.(seq . (k + 1)).| by XREAL_1:6;
( |.((Partial_Sums seq) . (k + 1)).| = |.(((Partial_Sums seq) . k) + (seq . (k + 1))).| & |.(((Partial_Sums seq) . k) + (seq . (k + 1))).| <= |.((Partial_Sums seq) . k).| + |.(seq . (k + 1)).| ) by COMPLEX1:56, SERIES_1:def 1;
then |.((Partial_Sums seq) . (k + 1)).| <= ((Partial_Sums |.seq.|) . k) + |.(seq . (k + 1)).| by A2, XXREAL_0:2;
then |.((Partial_Sums seq) . (k + 1)).| <= ((Partial_Sums |.seq.|) . k) + (|.seq.| . (k + 1)) by VALUED_1:18;
hence S1[k + 1] by SERIES_1:def 1; :: thesis: verum
end;
(Partial_Sums |.seq.|) . 0 = |.seq.| . 0 by SERIES_1:def 1
.= |.(seq . 0).| by VALUED_1:18 ;
then A3: S1[ 0 ] by SERIES_1:def 1;
for k being Nat holds S1[k] from NAT_1:sch 2(A3, A1);
 hence |.((Partial_Sums seq) . k).| <= (Partial_Sums |.seq.|) . k ; :: thesis: verum