let f be Function of [:NAT,NAT:],ExtREAL; 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; ( ( 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
; (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 S1[ 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:
S1[ 0 ]
by A1, A2, RINFSUP2:7;
A5:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A6:
S1[
n]
;
S1[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
S1[
n + 1]
by A6, A7, A8, XXREAL_3:36;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A4, A5);
hence
(Partial_Sums_in_cod2 f) . (i,k) <= (Partial_Sums_in_cod2 f) . (j,k)
; verum