let f be nonnegative Function of [:NAT,NAT:],ExtREAL; :: thesis: for m being Element of NAT holds ProjMap1 ((Partial_Sums_in_cod2 f),m) is non-decreasing
let m be Element of NAT ; :: thesis: ProjMap1 ((Partial_Sums_in_cod2 f),m) is non-decreasing
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

proof

let n, j be Nat; :: thesis: ( j <= n implies (ProjMap1 ((Partial_Sums_in_cod2 f),m)) . j <= (ProjMap1 ((Partial_Sums_in_cod2 f),m)) . n )
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)

proof

let k be Nat; :: thesis: (ProjMap1 ((Partial_Sums_in_cod2 f),m)) . k <= (ProjMap1 ((Partial_Sums_in_cod2 f),m)) . (k + 1)
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: verum

end;

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

proof

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

now :: thesis: ( k > j implies S₁[k] )

assume k > j ; :: thesis: S₁[k]
then A11: k >= j + 1 by NAT_1:13;

per cases ( k = j + 1 or k > j + 1 ) by A11, XXREAL_0:1;

suppose k = j + 1 ; :: thesis: S₁[k]

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

end;

suppose A12: k > j + 1 ; :: thesis: S₁[k]

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: verum

end;

end;

end;

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

end;

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

end;

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