let f be nonnegative Function of [:NAT,NAT:],ExtREAL; :: thesis: ( ( for i1, i2, j being Nat st i1 <= i2 holds
(Partial_Sums_in_cod1 f) . (i1,j) <= (Partial_Sums_in_cod1 f) . (i2,j) ) & ( for i, j1, j2 being Nat st j1 <= j2 holds
(Partial_Sums_in_cod2 f) . (i,j1) <= (Partial_Sums_in_cod2 f) . (i,j2) ) )

A2: now :: thesis: for i1, i2, j being natural number st i1 <= i2 holds
(Partial_Sums_in_cod1 f) . (i1,j) <= (Partial_Sums_in_cod1 f) . (i2,j)

let i1, i2, j be natural number ; :: thesis: ( i1 <= i2 implies (Partial_Sums_in_cod1 f) . (i1,j) <= (Partial_Sums_in_cod1 f) . (i2,j) )
assume i1 <= i2 ; :: thesis: (Partial_Sums_in_cod1 f) . (i1,j) <= (Partial_Sums_in_cod1 f) . (i2,j)
then consider k being Nat such that
A3: i2 = i1 + k by NAT_1:10;
defpred S₁[ Nat] means ( $1 <= k implies (Partial_Sums_in_cod1 f) . (i1,j) <= (Partial_Sums_in_cod1 f) . ((i1 + $1),j) );
A4: S₁[ 0 ] ;
A5: for l being Nat st S₁[l] holds
S₁[l + 1]

proof

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

now :: thesis: ( l + 1 <= k implies (Partial_Sums_in_cod1 f) . (i1,j) <= (Partial_Sums_in_cod1 f) . ((i1 + (l + 1)),j) )

assume A7: l + 1 <= k ; :: thesis: (Partial_Sums_in_cod1 f) . (i1,j) <= (Partial_Sums_in_cod1 f) . ((i1 + (l + 1)),j)
(Partial_Sums_in_cod1 f) . (((i1 + l) + 1),j) = ((Partial_Sums_in_cod1 f) . ((i1 + l),j)) + (f . (((i1 + l) + 1),j)) by DefRSM;
then (Partial_Sums_in_cod1 f) . ((i1 + l),j) <= (Partial_Sums_in_cod1 f) . (((i1 + l) + 1),j) by SUPINF_2:51, XXREAL_3:39;
hence (Partial_Sums_in_cod1 f) . (i1,j) <= (Partial_Sums_in_cod1 f) . ((i1 + (l + 1)),j) by A6, A7, NAT_1:13, XXREAL_0:2; :: thesis: verum

end;

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

end;

for l being Nat holds S₁[l] from NAT_1:sch 2(A4, A5);
hence (Partial_Sums_in_cod1 f) . (i1,j) <= (Partial_Sums_in_cod1 f) . (i2,j) by A3; :: thesis: verum

end;

now :: thesis: for i, j1, j2 being natural number st j1 <= j2 holds
(Partial_Sums_in_cod2 f) . (i,j1) <= (Partial_Sums_in_cod2 f) . (i,j2)

let i, j1, j2 be natural number ; :: thesis: ( j1 <= j2 implies (Partial_Sums_in_cod2 f) . (i,j1) <= (Partial_Sums_in_cod2 f) . (i,j2) )
assume j1 <= j2 ; :: thesis: (Partial_Sums_in_cod2 f) . (i,j1) <= (Partial_Sums_in_cod2 f) . (i,j2)
then consider k being Nat such that
B3: j2 = j1 + k by NAT_1:10;
defpred S₁[ Nat] means ( $1 <= k implies (Partial_Sums_in_cod2 f) . (i,j1) <= (Partial_Sums_in_cod2 f) . (i,(j1 + $1)) );
B4: S₁[ 0 ] ;
B5: for l being Nat st S₁[l] holds
S₁[l + 1]

proof

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

now :: thesis: ( l + 1 <= k implies (Partial_Sums_in_cod2 f) . (i,j1) <= (Partial_Sums_in_cod2 f) . (i,(j1 + (l + 1))) )

assume B7: l + 1 <= k ; :: thesis: (Partial_Sums_in_cod2 f) . (i,j1) <= (Partial_Sums_in_cod2 f) . (i,(j1 + (l + 1)))
(Partial_Sums_in_cod2 f) . (i,((j1 + l) + 1)) = ((Partial_Sums_in_cod2 f) . (i,(j1 + l))) + (f . (i,((j1 + l) + 1))) by DefCSM;
then (Partial_Sums_in_cod2 f) . (i,(j1 + l)) <= (Partial_Sums_in_cod2 f) . (i,((j1 + l) + 1)) by SUPINF_2:51, XXREAL_3:39;
hence (Partial_Sums_in_cod2 f) . (i,j1) <= (Partial_Sums_in_cod2 f) . (i,(j1 + (l + 1))) by B6, B7, NAT_1:13, XXREAL_0:2; :: thesis: verum

end;

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

end;

for l being Nat holds S₁[l] from NAT_1:sch 2(B4, B5);
hence (Partial_Sums_in_cod2 f) . (i,j1) <= (Partial_Sums_in_cod2 f) . (i,j2) by B3; :: thesis: verum

end;

hence ( ( for i1, i2, j being Nat st i1 <= i2 holds
(Partial_Sums_in_cod1 f) . (i1,j) <= (Partial_Sums_in_cod1 f) . (i2,j) ) & ( for i, j1, j2 being Nat st j1 <= j2 holds
(Partial_Sums_in_cod2 f) . (i,j1) <= (Partial_Sums_in_cod2 f) . (i,j2) ) ) by A2; :: thesis: verum