let seq be Complex_Sequence; :: thesis: for k being Element of NAT holds |.((Partial_Sums seq) . k).| <= (Partial_Sums |.seq.|) . k
let k be Element of NAT ; :: thesis: |.((Partial_Sums seq) . k).| <= (Partial_Sums |.seq.|) . k
defpred S₁[ Element of NAT ] means |.((Partial_Sums seq) . $1).| <= (Partial_Sums |.seq.|) . $1;
(Partial_Sums |.seq.|) . 0 = |.seq.| . 0 by SERIES_1:def 1
.= |.(seq . 0 ).| by VALUED_1:18 ;
then A1: S₁[ 0 ] by Def7;

A2: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
A4: |.((Partial_Sums seq) . (k + 1)).| = |.(((Partial_Sums seq) . k) + (seq . (k + 1))).| by Def7;
A5: |.(((Partial_Sums seq) . k) + (seq . (k + 1))).| <= |.((Partial_Sums seq) . k).| + |.(seq . (k + 1)).| by COMPLEX1:142;
|.((Partial_Sums seq) . k).| + |.(seq . (k + 1)).| <= ((Partial_Sums |.seq.|) . k) + |.(seq . (k + 1)).| by A3, XREAL_1:8;
then |.((Partial_Sums seq) . (k + 1)).| <= ((Partial_Sums |.seq.|) . k) + |.(seq . (k + 1)).| by A4, A5, XXREAL_0:2;
then |.((Partial_Sums seq) . (k + 1)).| <= ((Partial_Sums |.seq.|) . k) + (|.seq.| . (k + 1)) by VALUED_1:18;
hence S₁[k + 1] by SERIES_1:def 1; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A1, A2);
hence |.((Partial_Sums seq) . k).| <= (Partial_Sums |.seq.|) . k ; :: thesis: verum