let Rseq1, Rseq2 be Function of [:NAT,NAT:],REAL; :: thesis: ( 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) ) ) ; :: thesis: for i, j being Nat holds (Partial_Sums Rseq1) . (i,j) <= (Partial_Sums Rseq2) . (i,j)
let i, j be Nat; :: thesis: (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]
proof
let l be Nat; :: thesis: ( S2[l] implies S2[l + 1] )
assume S2[l] ; :: thesis: S2[l + 1]
( (Partial_Sums Rseq1) . ((l + 1),0) = (Partial_Sums_in_cod1 Rseq1) . ((l + 1),0) & (Partial_Sums Rseq2) . ((l + 1),0) = (Partial_Sums_in_cod1 Rseq2) . ((l + 1),0) ) by DefCS;
hence S2[l + 1] by a1, lm84a; :: thesis: verum
end;
for l being Nat holds S2[l] from NAT_1:sch 2(a4, a5);
 hence S1[ 0 ] ; :: thesis: verum
end;
a8: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A9: S1[k] ; :: thesis: 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; :: thesis: 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) ; :: thesis: verum