let s be Real_Sequence; :: thesis: for n being Nat holds |.((Partial_Sums s) . n).| <= (Partial_Sums (abs s)) . n
set s1 = abs s;
defpred S₁[ Nat] means |.((Partial_Sums s) . $1).| <= (Partial_Sums (abs s)) . $1;
let n be Nat; :: thesis: |.((Partial_Sums s) . n).| <= (Partial_Sums (abs s)) . n
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume |.((Partial_Sums s) . n).| <= (Partial_Sums (abs s)) . n ; :: thesis: S₁[n + 1]
then A2: |.((Partial_Sums s) . n).| + |.(s . (n + 1)).| <= ((Partial_Sums (abs s)) . n) + |.(s . (n + 1)).| by XREAL_1:6;
(Partial_Sums (abs s)) . (n + 1) = ((Partial_Sums (abs s)) . n) + ((abs s) . (n + 1)) by SERIES_1:def 1;
then A3: (Partial_Sums (abs s)) . (n + 1) = ((Partial_Sums (abs s)) . n) + |.(s . (n + 1)).| by SEQ_1:12;
( |.((Partial_Sums s) . (n + 1)).| = |.(((Partial_Sums s) . n) + (s . (n + 1))).| & |.(((Partial_Sums s) . n) + (s . (n + 1))).| <= |.((Partial_Sums s) . n).| + |.(s . (n + 1)).| ) by COMPLEX1:56, SERIES_1:def 1;
hence S₁[n + 1] by A3, A2, XXREAL_0:2; :: thesis: verum

end;

(abs s) . 0 = |.(s . 0).| by SEQ_1:12;
then (Partial_Sums (abs s)) . 0 = |.(s . 0).| by SERIES_1:def 1;
then A4: S₁[ 0 ] by SERIES_1:def 1;
for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A1);
hence |.((Partial_Sums s) . n).| <= (Partial_Sums (abs s)) . n ; :: thesis: verum