take f = <*> REAL; :: thesis: f is non-decreasing
let n be Element of NAT ; :: according to INTEGRA2:def 1 :: 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