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

proof

let n be 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;
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