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 S1[ Nat] means |.((Partial_Sums seq) . \$1).| <= (Partial_Sums (abs seq)) . \$1;
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
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 (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 ;
hence S1[k + 1] by SERIES_1:def 1; :: thesis: verum
end;
( (Partial_Sums (abs seq)) . 0 = (abs seq) . 0 & (abs seq) . 0 = |.(seq . 0).| ) by ;
then A4: S1[ 0 ] by SERIES_1:def 1;
for k being Nat holds S1[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