let r be Real; :: thesis: for n being Element of NAT
for seq being Real_Sequence st ( for m being Element of NAT st m <= n holds
seq . m <= r ) holds
for m being Element of NAT st m <= n holds
(Partial_Sums seq) . m <= r * (m + 1)
let n be Element of NAT ; :: thesis: for seq being Real_Sequence st ( for m being Element of NAT st m <= n holds
seq . m <= r ) holds
for m being Element of NAT st m <= n holds
(Partial_Sums seq) . m <= r * (m + 1)
let seq be Real_Sequence; :: thesis: ( ( for m being Element of NAT st m <= n holds
seq . m <= r ) implies for m being Element of NAT st m <= n holds
(Partial_Sums seq) . m <= r * (m + 1) )
assume A1: for m being Element of NAT st m <= n holds
seq . m <= r ; :: thesis: for m being Element of NAT st m <= n holds
(Partial_Sums seq) . m <= r * (m + 1)
defpred S₁[ Element of NAT ] means ( $1 <= n implies (Partial_Sums seq) . $1 <= r * ($1 + 1) );
A2: S₁[ 0 ]

proof

( (Partial_Sums seq) . 0 = seq . 0 & 0 <= n ) by SERIES_1:def 1;
hence S₁[ 0 ] by A1; :: thesis: verum

end;

A3: for m being Element of NAT st S₁[m] holds
S₁[m + 1]

proof

let m be Element of NAT ; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A4: S₁[m] ; :: thesis: S₁[m + 1]
assume m + 1 <= n ; :: thesis: (Partial_Sums seq) . (m + 1) <= r * ((m + 1) + 1)
then ( (Partial_Sums seq) . m <= r * (m + 1) & seq . (m + 1) <= r & (Partial_Sums seq) . (m + 1) = ((Partial_Sums seq) . m) + (seq . (m + 1)) ) by A1, A4, NAT_1:13, SERIES_1:def 1;
then (Partial_Sums seq) . (m + 1) <= (r * (m + 1)) + r by XREAL_1:9;
hence (Partial_Sums seq) . (m + 1) <= r * ((m + 1) + 1) ; :: thesis: verum

end;

for m being Element of NAT holds S₁[m] from NAT_1:sch 1(A2, A3);
hence for m being Element of NAT st m <= n holds
(Partial_Sums seq) . m <= r * (m + 1) ; :: thesis: verum