let r be Real; :: thesis: for n being Nat
for seq being Real_Sequence st ( for m being Nat st m <= n holds
seq . m <= r ) holds
for m being Nat st m <= n holds
(Partial_Sums seq) . m <= r * (m + 1)

let n be Nat; :: thesis: for seq being Real_Sequence st ( for m being Nat st m <= n holds
seq . m <= r ) holds
for m being Nat st m <= n holds
(Partial_Sums seq) . m <= r * (m + 1)

let seq be Real_Sequence; :: thesis: ( ( for m being Nat st m <= n holds
seq . m <= r ) implies for m being Nat st m <= n holds
(Partial_Sums seq) . m <= r * (m + 1) )

assume A1: for m being Nat st m <= n holds
seq . m <= r ; :: thesis: for m being Nat st m <= n holds
(Partial_Sums seq) . m <= r * (m + 1)

defpred S1[ Nat] means ( \$1 <= n implies (Partial_Sums seq) . \$1 <= r * (\$1 + 1) );
A2: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume A3: S1[m] ; :: thesis: S1[m + 1]
A4: (Partial_Sums seq) . (m + 1) = ((Partial_Sums seq) . m) + (seq . (m + 1)) by SERIES_1:def 1;
assume A5: m + 1 <= n ; :: thesis: (Partial_Sums seq) . (m + 1) <= r * ((m + 1) + 1)
then seq . (m + 1) <= r by A1;
then (Partial_Sums seq) . (m + 1) <= (r * (m + 1)) + r by ;
hence (Partial_Sums seq) . (m + 1) <= r * ((m + 1) + 1) ; :: thesis: verum
end;
(Partial_Sums seq) . 0 = seq . 0 by SERIES_1:def 1;
then A6: S1[ 0 ] by A1;
for m being Nat holds S1[m] from NAT_1:sch 2(A6, A2);
hence for m being Nat st m <= n holds
(Partial_Sums seq) . m <= r * (m + 1) ; :: thesis: verum