let f be FinSequence of REAL ; :: thesis: ( f is non-decreasing implies - f is non-increasing )
assume A1: f is non-decreasing ; :: thesis: - f is non-increasing
for n being Element of NAT st n in dom (- f) & n + 1 in dom (- f) holds
(- f) . n >= (- f) . (n + 1)

proof

let n be Element of NAT ; :: thesis: ( n in dom (- f) & n + 1 in dom (- f) implies (- f) . n >= (- f) . (n + 1) )
assume A2: ( n in dom (- f) & n + 1 in dom (- f) ) ; :: thesis: (- f) . n >= (- f) . (n + 1)
dom (- f) = dom f by VALUED_1:8;
then A3: f . n <= f . (n + 1) by A1, A2, INTEGRA2:def 1;
A4: (- f) . n = - (f . n) by RVSUM_1:35;
(- f) . (n + 1) = - (f . (n + 1)) by RVSUM_1:35;
hence (- f) . n >= (- f) . (n + 1) by A3, A4, XREAL_1:26; :: thesis: verum

end;

hence - f is non-increasing by RFINSEQ:def 4; :: thesis: verum