let f be PartFunc of NAT ,REAL ; :: thesis: ( f is non-decreasing & f is non-increasing implies f is constant )
assume A8: ( f is non-decreasing & f is non-increasing ) ; :: thesis: f is constant
let x be set ; :: according to FUNCT_1:def 16 :: thesis: for b₁ being set holds
( not x in dom f or not b₁ in dom f or f . x = f . b₁ )
let y be set ; :: thesis: ( not x in dom f or not y in dom f or f . x = f . y )
assume A9: ( 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 A9;
( m <= n or n <= m ) ;
then ( f . m <= f . n & f . n <= f . m ) by A8, A9, Def3, Def4;
hence f . x = f . y by XXREAL_0:1; :: thesis: verum