let f be PartFunc of NAT ,REAL ; :: thesis: ( f is non-decreasing & f is non-increasing implies f is constant )
assume A4: ( 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 proj1 f or not b₁ in proj1 f or f . x = f . b₁ )
let y be set ; :: thesis: ( not x in proj1 f or not y in proj1 f or f . x = f . y )
assume A5: ( 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 A5;
( m <= n or n <= m ) ;
then ( f . m <= f . n & f . n <= f . m ) by A4, A5, Def3, Def4;
hence f . x = f . y by XXREAL_0:1; :: thesis: verum