let seq be Real_Sequence; :: thesis: for k being Element of NAT holds abs ((Partial_Sums seq) . k) <= (Partial_Sums (abs seq)) . k
set PS = Partial_Sums seq;
set absPS = Partial_Sums (abs seq);
defpred S₁[ Element of NAT ] means abs ((Partial_Sums seq) . $1) <= (Partial_Sums (abs seq)) . $1;
A1: S₁[ 0 ]

proof

( (Partial_Sums (abs seq)) . 0 = (abs seq) . 0 & (abs seq) . 0 = abs (seq . 0 ) ) by SEQ_1:16, SERIES_1:def 1;
hence S₁[ 0 ] by SERIES_1:def 1; :: thesis: verum

end;

A2: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

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

end;

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