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

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume abs ((Partial_Sums s) . n) <= (Partial_Sums (abs s)) . n ; :: thesis: S₁[n + 1]
then A2: (abs ((Partial_Sums s) . n)) + (abs (s . (n + 1))) <= ((Partial_Sums (abs s)) . n) + (abs (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) + (abs (s . (n + 1))) by SEQ_1:12;
( abs ((Partial_Sums s) . (n + 1)) = abs (((Partial_Sums s) . n) + (s . (n + 1))) & abs (((Partial_Sums s) . n) + (s . (n + 1))) <= (abs ((Partial_Sums s) . n)) + (abs (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 = abs (s . 0) by SEQ_1:12;
then (Partial_Sums (abs s)) . 0 = abs (s . 0) by SERIES_1:def 1;
then A4: S₁[ 0 ] by SERIES_1:def 1;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A4, A1);
hence abs ((Partial_Sums s) . n) <= (Partial_Sums (abs s)) . n ; :: thesis: verum