let f be Real_Sequence; :: thesis: ( f is absolutely_summable implies abs (Sum f) <= Sum (abs f) )
defpred S₁[ Element of NAT ] means (abs (Partial_Sums f)) . $1 <= (Partial_Sums (abs f)) . $1;

A1: now

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then |.((Partial_Sums f) . n).| <= (Partial_Sums (abs f)) . n by SEQ_1:16;
then ( |.(((Partial_Sums f) . n) + (f . (n + 1))).| <= |.((Partial_Sums f) . n).| + |.(f . (n + 1)).| & |.((Partial_Sums f) . n).| + |.(f . (n + 1)).| <= ((Partial_Sums (abs f)) . n) + |.(f . (n + 1)).| ) by COMPLEX1:142, XREAL_1:8;
then |.(((Partial_Sums f) . n) + (f . (n + 1))).| <= ((Partial_Sums (abs f)) . n) + |.(f . (n + 1)).| by XXREAL_0:2;
then |.((Partial_Sums f) . (n + 1)).| <= ((Partial_Sums (abs f)) . n) + |.(f . (n + 1)).| by SERIES_1:def 1;
then (abs (Partial_Sums f)) . (n + 1) <= ((Partial_Sums (abs f)) . n) + |.(f . (n + 1)).| by SEQ_1:16;
then (abs (Partial_Sums f)) . (n + 1) <= ((Partial_Sums (abs f)) . n) + ((abs f) . (n + 1)) by SEQ_1:16;
hence S₁[n + 1] by SERIES_1:def 1; :: thesis: verum

end;

(abs (Partial_Sums f)) . 0 = abs ((Partial_Sums f) . 0) by SEQ_1:16
.= abs (f . 0) by SERIES_1:def 1
.= (abs f) . 0 by SEQ_1:16 ;
then A2: S₁[ 0 ] by SERIES_1:def 1;
A3: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A2, A1);
assume A4: f is absolutely_summable ; :: thesis: abs (Sum f) <= Sum (abs f)
then abs f is summable by SERIES_1:def 5;
then A5: Partial_Sums (abs f) is convergent by SERIES_1:def 2;
f is summable by A4, SERIES_1:40;
then A6: Partial_Sums f is convergent by SERIES_1:def 2;
then abs (Partial_Sums f) is convergent by SEQ_4:26;
then lim (abs (Partial_Sums f)) <= lim (Partial_Sums (abs f)) by A5, A3, SEQ_2:32;
then abs (lim (Partial_Sums f)) <= lim (Partial_Sums (abs f)) by A6, SEQ_4:27;
then abs (lim (Partial_Sums f)) <= Sum (abs f) by SERIES_1:def 3;
hence abs (Sum f) <= Sum (abs f) by SERIES_1:def 3; :: thesis: verum