let f be Function of [:NAT,NAT:],ExtREAL; :: thesis: for i, j, k being Nat st ( for n being Element of NAT holds ProjMap1 (f,n) is non-decreasing ) & i <= j holds
(Partial_Sums_in_cod1 f) . (k,i) <= (Partial_Sums_in_cod1 f) . (k,j)
let i, j, k be Nat; :: thesis: ( ( for n being Element of NAT holds ProjMap1 (f,n) is non-decreasing ) & i <= j implies (Partial_Sums_in_cod1 f) . (k,i) <= (Partial_Sums_in_cod1 f) . (k,j) )
assume that
A1: for n being Element of NAT holds ProjMap1 (f,n) is non-decreasing and
A2: i <= j ; :: thesis: (Partial_Sums_in_cod1 f) . (k,i) <= (Partial_Sums_in_cod1 f) . (k,j)
for n being Element of NAT holds ProjMap2 ((~ f),n) is non-decreasing
proof
let n be Element of NAT ; :: thesis: ProjMap2 ((~ f),n) is non-decreasing
ProjMap1 (f,n) = ProjMap2 ((~ f),n) by Th32;
hence ProjMap2 ((~ f),n) is non-decreasing by A1; :: thesis: verum
end;
then (Partial_Sums_in_cod2 (~ f)) . (i,k) <= (Partial_Sums_in_cod2 (~ f)) . (j,k) by A2, Th89;
then (Partial_Sums_in_cod1 f) . (k,i) <= (Partial_Sums_in_cod2 (~ f)) . (j,k) by Th39;
hence (Partial_Sums_in_cod1 f) . (k,i) <= (Partial_Sums_in_cod1 f) . (k,j) by Th39; :: thesis: verum