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

proof

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

end;

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