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
(Partial_Sums rseq1) . m <= p * ((Partial_Sums rseq2) . m)
let m be Nat; :: thesis: for p being Real st ( for n being Nat st n <= m holds
rseq1 . n <= p * (rseq2 . n) ) holds
(Partial_Sums rseq1) . m <= p * ((Partial_Sums rseq2) . m)
let p be Real; :: thesis: ( ( for n being Nat st n <= m holds
rseq1 . n <= p * (rseq2 . n) ) implies (Partial_Sums rseq1) . m <= p * ((Partial_Sums rseq2) . m) )
defpred S₁[ Nat] means ( $1 <= m implies (Partial_Sums rseq1) . $1 <= p * ((Partial_Sums rseq2) . $1) );
assume A1: for n being Nat st n <= m holds
rseq1 . n <= p * (rseq2 . n) ; :: thesis: (Partial_Sums rseq1) . m <= p * ((Partial_Sums rseq2) . m)

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

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]

now :: thesis: ( n + 1 <= m implies (Partial_Sums rseq1) . (n + 1) <= p * ((Partial_Sums rseq2) . (n + 1)) )

assume A4: n + 1 <= m ; :: thesis: (Partial_Sums rseq1) . (n + 1) <= p * ((Partial_Sums rseq2) . (n + 1))
then rseq1 . (n + 1) <= p * (rseq2 . (n + 1)) by A1;
then A5: (p * ((Partial_Sums rseq2) . n)) + (rseq1 . (n + 1)) <= (p * ((Partial_Sums rseq2) . n)) + (p * (rseq2 . (n + 1))) by XREAL_1:6;
( n < n + 1 & (Partial_Sums rseq1) . (n + 1) = ((Partial_Sums rseq1) . n) + (rseq1 . (n + 1)) ) by SERIES_1:def 1, XREAL_1:29;
then A6: (Partial_Sums rseq1) . (n + 1) <= (p * ((Partial_Sums rseq2) . n)) + (rseq1 . (n + 1)) by A3, A4, XREAL_1:6, XXREAL_0:2;
(p * ((Partial_Sums rseq2) . n)) + (p * (rseq2 . (n + 1))) = p * (((Partial_Sums rseq2) . n) + (rseq2 . (n + 1)))
.= p * ((Partial_Sums rseq2) . (n + 1)) by SERIES_1:def 1 ;
hence (Partial_Sums rseq1) . (n + 1) <= p * ((Partial_Sums rseq2) . (n + 1)) by A6, A5, XXREAL_0:2; :: thesis: verum

end;

hence S₁[n + 1] ; :: thesis: verum

end;

A7: S₁[ 0 ]

proof

assume 0 <= m ; :: thesis: (Partial_Sums rseq1) . 0 <= p * ((Partial_Sums rseq2) . 0)
( (Partial_Sums rseq1) . 0 = rseq1 . 0 & p * ((Partial_Sums rseq2) . 0) = p * (rseq2 . 0) ) by SERIES_1:def 1;
hence (Partial_Sums rseq1) . 0 <= p * ((Partial_Sums rseq2) . 0) by A1; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A7, A2);
hence (Partial_Sums rseq1) . m <= p * ((Partial_Sums rseq2) . m) ; :: thesis: verum