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

proof

assume 0 <= m ; :: thesis: (Partial_Sums rseq1) . 0 <= p * ((Partial_Sums rseq2) . 0 )
A3: (Partial_Sums rseq1) . 0 = rseq1 . 0 by SERIES_1:def 1;
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, A3; :: thesis: verum

end;

A4: now

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A5: S₁[n] ; :: thesis: S₁[n + 1]

now

assume A6: n + 1 <= m ; :: thesis: (Partial_Sums rseq1) . (n + 1) <= p * ((Partial_Sums rseq2) . (n + 1))
A7: n < n + 1 by XREAL_1:31;
A8: (Partial_Sums rseq1) . (n + 1) = ((Partial_Sums rseq1) . n) + (rseq1 . (n + 1)) by SERIES_1:def 1;
A9: rseq1 . (n + 1) <= p * (rseq2 . (n + 1)) by A1, A6;
A10: (Partial_Sums rseq1) . (n + 1) <= (p * ((Partial_Sums rseq2) . n)) + (rseq1 . (n + 1)) by A5, A6, A7, A8, XREAL_1:8, XXREAL_0:2;
A11: (p * ((Partial_Sums rseq2) . n)) + (rseq1 . (n + 1)) <= (p * ((Partial_Sums rseq2) . n)) + (p * (rseq2 . (n + 1))) by A9, XREAL_1:8;
(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 A10, A11, XXREAL_0:2; :: thesis: verum

end;

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

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A2, A4);
hence (Partial_Sums rseq1) . m <= p * ((Partial_Sums rseq2) . m) ; :: thesis: verum