let f be nonnegative Function of [:NAT,NAT:],ExtREAL; :: thesis:
let m be Element of NAT ; :: thesis:
set PS = ProjMap1 ((Partial_Sums_in_cod2 f),m);
for n, j being Nat st j <= n holds
(ProjMap1 ((Partial_Sums_in_cod2 f),m)) . j <= (ProjMap1 ((Partial_Sums_in_cod2 f),m)) . n

let n, j be Nat; :: thesis:
defpred S₁[ Nat] means (ProjMap1 ((Partial_Sums_in_cod2 f),m)) . j <= (ProjMap1 ((Partial_Sums_in_cod2 f),m)) . $1;
A6: for k being Nat holds (ProjMap1 ((Partial_Sums_in_cod2 f),m)) . k <= (ProjMap1 ((Partial_Sums_in_cod2 f),m)) . (k + 1)

let k be Nat; :: thesis:
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
(ProjMap1 ((Partial_Sums_in_cod2 f),m)) . (k + 1) = (Partial_Sums_in_cod2 f) . (m,(k + 1)) by MESFUNC9:def 6
.= ((Partial_Sums_in_cod2 f) . (m,k1)) + (f . (m,(k + 1))) by DefCSM
.= ((ProjMap1 ((Partial_Sums_in_cod2 f),m)) . k) + (f . (m,(k + 1))) by MESFUNC9:def 6 ;
hence (ProjMap1 ((Partial_Sums_in_cod2 f),m)) . k <= (ProjMap1 ((Partial_Sums_in_cod2 f),m)) . (k + 1) by SUPINF_2:51, XXREAL_3:39; :: thesis:

end;

A8: for k being Nat st k >= j & ( for l being Nat st l >= j & l < k holds
S₁[l] ) holds
S₁[k]

let k be Nat; :: thesis:
assume that
A9: k >= j and
A10: for l being Nat st l >= j & l < k holds
S₁[l] ; :: thesis:

assume k > j ; :: thesis:
then A11: k >= j + 1 by NAT_1:13;

per cases by A11, XXREAL_0:1;

suppose k = j + 1 ; :: thesis:

hence S₁[k] by A6; :: thesis:

end;

suppose A12: k > j + 1 ; :: thesis:

then reconsider l = k - 1 as Element of NAT by NAT_1:20;
k < k + 1 by NAT_1:13;
then A13: k > l by XREAL_1:19;
k = l + 1 ;
then A14: (ProjMap1 ((Partial_Sums_in_cod2 f),m)) . l <= (ProjMap1 ((Partial_Sums_in_cod2 f),m)) . k by A6;
(ProjMap1 ((Partial_Sums_in_cod2 f),m)) . j <= (ProjMap1 ((Partial_Sums_in_cod2 f),m)) . l by A10, A13, A12, XREAL_1:19;
hence S₁[k] by A14, XXREAL_0:2; :: thesis:

end;

end;

end;

hence S₁[k] by A9, XXREAL_0:1; :: thesis:

end;

A15: for k being Nat st k >= j holds
S₁[k] from NAT_1:sch 9(A8);
assume j <= n ; :: thesis:
hence (ProjMap1 ((Partial_Sums_in_cod2 f),m)) . j <= (ProjMap1 ((Partial_Sums_in_cod2 f),m)) . n by A15; :: thesis:

end;

hence ProjMap1 ((Partial_Sums_in_cod2 f),m) is non-decreasing by RINFSUP2:7; :: thesis: