let rseq be Real_Sequence; :: thesis: for p being Real st ( for n being Element of NAT holds rseq . n <= p ) holds
for n, l being Element of NAT holds ((Partial_Sums rseq) . (n + l)) - ((Partial_Sums rseq) . n) <= p * l
let p be Real; :: thesis: ( ( for n being Element of NAT holds rseq . n <= p ) implies for n, l being Element of NAT holds ((Partial_Sums rseq) . (n + l)) - ((Partial_Sums rseq) . n) <= p * l )
assume A1: for n being Element of NAT holds rseq . n <= p ; :: thesis: for n, l being Element of NAT holds ((Partial_Sums rseq) . (n + l)) - ((Partial_Sums rseq) . n) <= p * l

now

let n be Element of NAT ; :: thesis: for l being Element of NAT holds S₁[l]
defpred S₁[ Element of NAT ] means ((Partial_Sums rseq) . (n + $1)) - ((Partial_Sums rseq) . n) <= p * $1;

A2: now

let l be Element of 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:8;
((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:8;
hence S₁[l + 1] by A4, XXREAL_0:2; :: thesis: verum

end;

A5: S₁[ 0 ] ;
thus for l being Element of NAT holds S₁[l] from NAT_1:sch 1(A5, A2); :: thesis: verum

end;

hence for n, l being Element of NAT holds ((Partial_Sums rseq) . (n + l)) - ((Partial_Sums rseq) . n) <= p * l ; :: thesis: verum