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
(abs s) . 0 = abs (s . 0 ) by SEQ_1:16;
then (Partial_Sums (abs s)) . 0 = abs (s . 0 ) by SERIES_1:def 1;
then A1: S₁[ 0 ] by SERIES_1:def 1;
A2: 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 A3: abs ((Partial_Sums s) . n) <= (Partial_Sums (abs s)) . n ; :: thesis: S₁[n + 1]
A4: abs ((Partial_Sums s) . (n + 1)) = abs (((Partial_Sums s) . n) + (s . (n + 1))) by SERIES_1:def 1;
A5: abs (((Partial_Sums s) . n) + (s . (n + 1))) <= (abs ((Partial_Sums s) . n)) + (abs (s . (n + 1))) by COMPLEX1:142;
(Partial_Sums (abs s)) . (n + 1) = ((Partial_Sums (abs s)) . n) + ((abs s) . (n + 1)) by SERIES_1:def 1;
then A6: (Partial_Sums (abs s)) . (n + 1) = ((Partial_Sums (abs s)) . n) + (abs (s . (n + 1))) by SEQ_1:16;
(abs ((Partial_Sums s) . n)) + (abs (s . (n + 1))) <= ((Partial_Sums (abs s)) . n) + (abs (s . (n + 1))) by A3, XREAL_1:8;
hence S₁[n + 1] by A4, A5, A6, XXREAL_0:2; :: thesis: verum

end;

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