take f = <*> REAL; :: thesis: f is non-increasing
let n be Element of NAT ; :: according to RFINSEQ:def 3 :: thesis: ( n in dom f & n + 1 in dom f implies f . n >= f . (n + 1) )
assume that
A1: n in dom f and
n + 1 in dom f ; :: thesis: f . n >= f . (n + 1)
thus f . n >= f . (n + 1) by A1; :: thesis: verum