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