let f be Function of [:NAT,NAT:],ExtREAL; :: thesis: for i, j, k being Nat st ( for m being Element of NAT holds ProjMap2 (f,m) is non-decreasing ) & i <= j holds
(Partial_Sums_in_cod2 f) . (i,k) <= (Partial_Sums_in_cod2 f) . (j,k)
let i, j, k be Nat; :: thesis: ( ( for m being Element of NAT holds ProjMap2 (f,m) is non-decreasing ) & i <= j implies (Partial_Sums_in_cod2 f) . (i,k) <= (Partial_Sums_in_cod2 f) . (j,k) )
assume that
A1: for m being Element of NAT holds ProjMap2 (f,m) is non-decreasing and
A2: i <= j ; :: thesis: (Partial_Sums_in_cod2 f) . (i,k) <= (Partial_Sums_in_cod2 f) . (j,k)
reconsider i1 = i, j1 = j as Element of NAT by ORDINAL1:def 12;
defpred S₁[ Nat] means (Partial_Sums_in_cod2 f) . (i,$1) <= (Partial_Sums_in_cod2 f) . (j,$1);
( (ProjMap2 (f,0)) . i1 = f . (i,0) & (ProjMap2 (f,0)) . j1 = f . (j,0) ) by MESFUNC9:def 7;
then ( (ProjMap2 (f,0)) . i1 = (Partial_Sums_in_cod2 f) . (i,0) & (ProjMap2 (f,0)) . j1 = (Partial_Sums_in_cod2 f) . (j,0) ) by DefCSM;
then A4: S₁[ 0 ] by A1, A2, RINFSUP2:7;
A5: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A6: S₁[n] ; :: thesis: S₁[n + 1]
A7: ( (Partial_Sums_in_cod2 f) . (i,(n + 1)) = ((Partial_Sums_in_cod2 f) . (i,n)) + (f . (i,(n + 1))) & (Partial_Sums_in_cod2 f) . (j,(n + 1)) = ((Partial_Sums_in_cod2 f) . (j,n)) + (f . (j,(n + 1))) ) by DefCSM;
A8: (ProjMap2 (f,(n + 1))) . i <= (ProjMap2 (f,(n + 1))) . j by A1, A2, RINFSUP2:7;
( (ProjMap2 (f,(n + 1))) . i1 = f . (i,(n + 1)) & (ProjMap2 (f,(n + 1))) . j1 = f . (j,(n + 1)) ) by MESFUNC9:def 7;
hence S₁[n + 1] by A6, A7, A8, XXREAL_3:36; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A5);
hence (Partial_Sums_in_cod2 f) . (i,k) <= (Partial_Sums_in_cod2 f) . (j,k) ; :: thesis: verum