let f be nonnegative V183() Function of [:NAT,NAT:],ExtREAL; :: thesis: for n being Element of NAT holds ProjMap2 ((Partial_Sums_in_cod1 f),n) is non-decreasing
let n be Element of NAT ; :: thesis: ProjMap2 ((Partial_Sums_in_cod1 f),n) is non-decreasing
A1: ProjMap1 ((Partial_Sums_in_cod2 (~ f)),n) is non-decreasing by Th63;
Partial_Sums_in_cod2 (~ f) = ~ (Partial_Sums_in_cod1 f) by Th40;
hence ProjMap2 ((Partial_Sums_in_cod1 f),n) is non-decreasing by A1, Th33; :: thesis: verum