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 S_{1}[ Nat] means ( $1 <= n implies (Partial_Sums seq) . $1 <= r * ($1 + 1) );

A2: for m being Nat st S_{1}[m] holds

S_{1}[m + 1]

then A6: S_{1}[ 0 ]
by A1;

for m being Nat holds S_{1}[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

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 S

A2: for m being Nat st S

S

proof

(Partial_Sums seq) . 0 = seq . 0
by SERIES_1:def 1;
let m be Nat; :: thesis: ( S_{1}[m] implies S_{1}[m + 1] )

assume A3: S_{1}[m]
; :: thesis: S_{1}[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 A3, A5, A4, NAT_1:13, XREAL_1:7;

hence (Partial_Sums seq) . (m + 1) <= r * ((m + 1) + 1) ; :: thesis: verum

end;assume A3: S

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 A3, A5, A4, NAT_1:13, XREAL_1:7;

hence (Partial_Sums seq) . (m + 1) <= r * ((m + 1) + 1) ; :: thesis: verum

then A6: S

for m being Nat holds S

hence for m being Nat st m <= n holds

(Partial_Sums seq) . m <= r * (m + 1) ; :: thesis: verum