let seq be Real_Sequence; :: thesis: for k being Nat holds |.((Partial_Sums seq) . k).| <= (Partial_Sums (abs seq)) . k

set PS = Partial_Sums seq;

set absPS = Partial_Sums (abs seq);

defpred S_{1}[ Nat] means |.((Partial_Sums seq) . $1).| <= (Partial_Sums (abs seq)) . $1;

A1: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

then A4: S_{1}[ 0 ]
by SERIES_1:def 1;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A4, A1);

hence for k being Nat holds |.((Partial_Sums seq) . k).| <= (Partial_Sums (abs seq)) . k ; :: thesis: verum

set PS = Partial_Sums seq;

set absPS = Partial_Sums (abs seq);

defpred S

A1: for k being Nat st S

S

proof

( (Partial_Sums (abs seq)) . 0 = (abs seq) . 0 & (abs seq) . 0 = |.(seq . 0).| )
by SEQ_1:12, SERIES_1:def 1;
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume S_{1}[k]
; :: thesis: S_{1}[k + 1]

then A2: |.((Partial_Sums seq) . k).| + |.(seq . (k + 1)).| <= ((Partial_Sums (abs seq)) . k) + |.(seq . (k + 1)).| by XREAL_1:7;

(Partial_Sums seq) . (k + 1) = ((Partial_Sums seq) . k) + (seq . (k + 1)) by SERIES_1:def 1;

then A3: |.((Partial_Sums seq) . (k + 1)).| <= |.((Partial_Sums seq) . k).| + |.(seq . (k + 1)).| by COMPLEX1:56;

(abs seq) . (k + 1) = |.(seq . (k + 1)).| by SEQ_1:12;

then |.((Partial_Sums seq) . (k + 1)).| <= ((Partial_Sums (abs seq)) . k) + ((abs seq) . (k + 1)) by A3, A2, XXREAL_0:2;

hence S_{1}[k + 1]
by SERIES_1:def 1; :: thesis: verum

end;assume S

then A2: |.((Partial_Sums seq) . k).| + |.(seq . (k + 1)).| <= ((Partial_Sums (abs seq)) . k) + |.(seq . (k + 1)).| by XREAL_1:7;

(Partial_Sums seq) . (k + 1) = ((Partial_Sums seq) . k) + (seq . (k + 1)) by SERIES_1:def 1;

then A3: |.((Partial_Sums seq) . (k + 1)).| <= |.((Partial_Sums seq) . k).| + |.(seq . (k + 1)).| by COMPLEX1:56;

(abs seq) . (k + 1) = |.(seq . (k + 1)).| by SEQ_1:12;

then |.((Partial_Sums seq) . (k + 1)).| <= ((Partial_Sums (abs seq)) . k) + ((abs seq) . (k + 1)) by A3, A2, XXREAL_0:2;

hence S

then A4: S

for k being Nat holds S

hence for k being Nat holds |.((Partial_Sums seq) . k).| <= (Partial_Sums (abs seq)) . k ; :: thesis: verum