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 S1[ Nat] means ( $1 <= k implies (Partial_Sums_in_cod1 f) . (i1,j) <= (Partial_Sums_in_cod1 f) . ((i1 + $1),j) );
A4: S1[ 0 ] ;
A5: for l being Nat st S1[l] holds
S1[l + 1]
proof
let l be Nat; :: thesis: ( S1[l] implies S1[l + 1] )
assume A6: S1[l] ; :: thesis: S1[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 S1[l + 1] ; :: thesis: verum
end;
for l being Nat holds S1[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 S1[ Nat] means ( $1 <= k implies (Partial_Sums_in_cod2 f) . (i,j1) <= (Partial_Sums_in_cod2 f) . (i,(j1 + $1)) );
B4: S1[ 0 ] ;
B5: for l being Nat st S1[l] holds
S1[l + 1]
proof
let l be Nat; :: thesis: ( S1[l] implies S1[l + 1] )
assume B6: S1[l] ; :: thesis: S1[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 S1[l + 1] ; :: thesis: verum
end;
for l being Nat holds S1[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