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) )
A2: dom (- f) = dom f by VALUED_1:8;
A3: ( (- f) . n = - (f . n) & (- f) . (n + 1) = - (f . (n + 1)) ) by RVSUM_1:17;
assume ( n in dom (- f) & n + 1 in dom (- f) ) ; :: thesis: (- f) . n >= (- f) . (n + 1)
then f . n <= f . (n + 1) by A1, A2, INTEGRA2:def 1;
hence (- f) . n >= (- f) . (n + 1) by A3, XREAL_1:24; :: thesis: verum

end;

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