let Rseq1, Rseq2 be Function of [:NAT,NAT:],REAL; ( Rseq1 is nonnegative-yielding & ( for n, m being Nat holds Rseq1 . (n,m) <= Rseq2 . (n,m) ) implies for i, j being Nat holds (Partial_Sums Rseq1) . (i,j) <= (Partial_Sums Rseq2) . (i,j) )
set RPS1 = Partial_Sums Rseq1;
set RPS2 = Partial_Sums Rseq2;
assume a1:
( Rseq1 is nonnegative-yielding & ( for n, m being Nat holds Rseq1 . (n,m) <= Rseq2 . (n,m) ) )
; for i, j being Nat holds (Partial_Sums Rseq1) . (i,j) <= (Partial_Sums Rseq2) . (i,j)
let i, j be Nat; (Partial_Sums Rseq1) . (i,j) <= (Partial_Sums Rseq2) . (i,j)
defpred S1[ Nat] means (Partial_Sums Rseq1) . (i,$1) <= (Partial_Sums Rseq2) . (i,$1);
a2:
S1[ 0 ]
proof
defpred S2[
Nat]
means (Partial_Sums Rseq1) . ($1,
0)
<= (Partial_Sums Rseq2) . ($1,
0);
a3:
(Partial_Sums Rseq1) . (
0,
0) =
(Partial_Sums_in_cod1 Rseq1) . (
0,
0)
by DefCS
.=
Rseq1 . (
0,
0)
by DefRS
;
(Partial_Sums Rseq2) . (
0,
0) =
(Partial_Sums_in_cod1 Rseq2) . (
0,
0)
by DefCS
.=
Rseq2 . (
0,
0)
by DefRS
;
then a4:
S2[
0 ]
by a1, a3;
a5:
for
l being
Nat st
S2[
l] holds
S2[
l + 1]
for
l being
Nat holds
S2[
l]
from NAT_1:sch 2(a4, a5);
hence
S1[
0 ]
;
verum
end;
a8:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A9:
S1[
k]
;
S1[k + 1]
a10:
(Partial_Sums_in_cod1 Rseq1) . (
i,
(k + 1))
<= (Partial_Sums_in_cod1 Rseq2) . (
i,
(k + 1))
by a1, lm84a;
(Partial_Sums Rseq1) . (
i,
(k + 1))
= ((Partial_Sums_in_cod1 Rseq1) . (i,(k + 1))) + ((Partial_Sums Rseq1) . (i,k))
by DefCS;
then
(Partial_Sums Rseq1) . (
i,
(k + 1))
<= ((Partial_Sums_in_cod1 Rseq2) . (i,(k + 1))) + ((Partial_Sums Rseq2) . (i,k))
by A9, a10, XREAL_1:7;
hence
S1[
k + 1]
by DefCS;
verum
end;
for k being Nat holds S1[k]
from NAT_1:sch 2(a2, a8);
hence
(Partial_Sums Rseq1) . (i,j) <= (Partial_Sums Rseq2) . (i,j)
; verum