let rseq be Real_Sequence; :: thesis: for p being Real st ( for n being Nat holds rseq . n <= p ) holds
for n, l being Nat holds ((Partial_Sums rseq) . (n + l)) - ((Partial_Sums rseq) . n) <= p * l
let p be Real; :: thesis: ( ( for n being Nat holds rseq . n <= p ) implies for n, l being Nat holds ((Partial_Sums rseq) . (n + l)) - ((Partial_Sums rseq) . n) <= p * l )
assume A1: for n being Nat holds rseq . n <= p ; :: thesis: for n, l being Nat holds ((Partial_Sums rseq) . (n + l)) - ((Partial_Sums rseq) . n) <= p * l
let n be Nat; :: thesis: for l being Nat holds ((Partial_Sums rseq) . (n + l)) - ((Partial_Sums rseq) . n) <= p * l
defpred S₁[ Nat] means ((Partial_Sums rseq) . (n + $1)) - ((Partial_Sums rseq) . n) <= p * $1;

A2: now :: thesis: for l being Nat st S₁[l] holds
S₁[l + 1]

let l be Nat; :: thesis: ( S₁[l] implies S₁[l + 1] )
assume A3: S₁[l] ; :: thesis: S₁[l + 1]
rseq . ((n + l) + 1) <= p by A1;
then A4: (p * l) + (rseq . ((n + l) + 1)) <= (p * l) + p by XREAL_1:6;
((Partial_Sums rseq) . (n + (l + 1))) - ((Partial_Sums rseq) . n) = (((Partial_Sums rseq) . (n + l)) + (rseq . ((n + l) + 1))) - ((Partial_Sums rseq) . n) by SERIES_1:def 1
.= (((Partial_Sums rseq) . (n + l)) - ((Partial_Sums rseq) . n)) + (rseq . ((n + l) + 1)) ;
then ((Partial_Sums rseq) . (n + (l + 1))) - ((Partial_Sums rseq) . n) <= (p * l) + (rseq . ((n + l) + 1)) by A3, XREAL_1:6;
hence S₁[l + 1] by A4, XXREAL_0:2; :: thesis: verum

end;

A5: S₁[ 0 ] ;
thus for l being Nat holds S₁[l] from NAT_1:sch 2(A5, A2); :: thesis: verum