let Rseq1, Rseq2 be Function of [:NAT,NAT:],REAL; :: thesis: ( ( for n, m being Nat holds Rseq1 . (n,m) <= Rseq2 . (n,m) ) implies for i, j being Nat holds
( (Partial_Sums_in_cod1 Rseq1) . (i,j) <= (Partial_Sums_in_cod1 Rseq2) . (i,j) & (Partial_Sums_in_cod2 Rseq1) . (i,j) <= (Partial_Sums_in_cod2 Rseq2) . (i,j) ) )
set RS1 = Partial_Sums_in_cod1 Rseq1;
set RS2 = Partial_Sums_in_cod1 Rseq2;
set CS1 = Partial_Sums_in_cod2 Rseq1;
set CS2 = Partial_Sums_in_cod2 Rseq2;
assume a1: for n, m being Nat holds Rseq1 . (n,m) <= Rseq2 . (n,m) ; :: thesis: for i, j being Nat holds
( (Partial_Sums_in_cod1 Rseq1) . (i,j) <= (Partial_Sums_in_cod1 Rseq2) . (i,j) & (Partial_Sums_in_cod2 Rseq1) . (i,j) <= (Partial_Sums_in_cod2 Rseq2) . (i,j) )
let i, j be Nat; :: thesis: ( (Partial_Sums_in_cod1 Rseq1) . (i,j) <= (Partial_Sums_in_cod1 Rseq2) . (i,j) & (Partial_Sums_in_cod2 Rseq1) . (i,j) <= (Partial_Sums_in_cod2 Rseq2) . (i,j) )
defpred S1[ Nat] means (Partial_Sums_in_cod1 Rseq1) . ($1,j) <= (Partial_Sums_in_cod1 Rseq2) . ($1,j);
( (Partial_Sums_in_cod1 Rseq1) . (0,j) = Rseq1 . (0,j) & (Partial_Sums_in_cod1 Rseq2) . (0,j) = Rseq2 . (0,j) ) by DefRS;
then a2: S1[ 0 ] by a1;
a3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume S1[k] ; :: thesis: S1[k + 1]
then a4: ( (Partial_Sums_in_cod1 Rseq1) . (k,j) <= (Partial_Sums_in_cod1 Rseq2) . (k,j) & Rseq1 . ((k + 1),j) <= Rseq2 . ((k + 1),j) ) by a1;
( (Partial_Sums_in_cod1 Rseq1) . ((k + 1),j) = ((Partial_Sums_in_cod1 Rseq1) . (k,j)) + (Rseq1 . ((k + 1),j)) & (Partial_Sums_in_cod1 Rseq2) . ((k + 1),j) = ((Partial_Sums_in_cod1 Rseq2) . (k,j)) + (Rseq2 . ((k + 1),j)) ) by DefRS;
hence S1[k + 1] by a4, XREAL_1:7; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(a2, a3);
 hence (Partial_Sums_in_cod1 Rseq1) . (i,j) <= (Partial_Sums_in_cod1 Rseq2) . (i,j) ; :: thesis: (Partial_Sums_in_cod2 Rseq1) . (i,j) <= (Partial_Sums_in_cod2 Rseq2) . (i,j)
defpred S2[ Nat] means (Partial_Sums_in_cod2 Rseq1) . (i,$1) <= (Partial_Sums_in_cod2 Rseq2) . (i,$1);
( (Partial_Sums_in_cod2 Rseq1) . (i,0) = Rseq1 . (i,0) & (Partial_Sums_in_cod2 Rseq2) . (i,0) = Rseq2 . (i,0) ) by DefCS;
then a5: S2[ 0 ] by a1;
a6: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume S2[k] ; :: thesis: S2[k + 1]
then a7: ( (Partial_Sums_in_cod2 Rseq1) . (i,k) <= (Partial_Sums_in_cod2 Rseq2) . (i,k) & Rseq1 . (i,(k + 1)) <= Rseq2 . (i,(k + 1)) ) by a1;
( (Partial_Sums_in_cod2 Rseq1) . (i,(k + 1)) = ((Partial_Sums_in_cod2 Rseq1) . (i,k)) + (Rseq1 . (i,(k + 1))) & (Partial_Sums_in_cod2 Rseq2) . (i,(k + 1)) = ((Partial_Sums_in_cod2 Rseq2) . (i,k)) + (Rseq2 . (i,(k + 1))) ) by DefCS;
hence S2[k + 1] by a7, XREAL_1:7; :: thesis: verum
end;
for k being Nat holds S2[k] from NAT_1:sch 2(a5, a6);
 hence (Partial_Sums_in_cod2 Rseq1) . (i,j) <= (Partial_Sums_in_cod2 Rseq2) . (i,j) ; :: thesis: verum