let f be PartFunc of NAT,REAL; :: thesis: ( f is non-decreasing & f is non-increasing implies f is constant )
assume A1: ( f is non-decreasing & f is non-increasing ) ; :: thesis: f is constant
let x, y be object ; :: according to FUNCT_1:def 10 :: thesis: ( not x in dom f or not y in dom f or f . x = f . y )
assume A2: ( x in dom f & y in dom f ) ; :: thesis: f . x = f . y
dom f c= NAT by RELAT_1:def 18;
then reconsider m = x, n = y as Element of NAT by A2;
( m <= n or n <= m ) ;
then ( f . m <= f . n & f . n <= f . m ) by A1, A2;
hence f . x = f . y by XXREAL_0:1; :: thesis: verum