let h be PartFunc of REAL ,REAL ; :: thesis: ( h is constant implies ( h is non-increasing & h is non-decreasing ) )
assume Z: h is constant ; :: thesis: ( h is non-increasing & h is non-decreasing )
thus h is non-increasing :: thesis: h is non-decreasing

proof

let r1 be Element of REAL ; :: according to RFUNCT_2:def 5 :: thesis: for r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r2 <= h . r1
let r2 be Element of REAL ; :: thesis: ( r1 in dom h & r2 in dom h & r1 < r2 implies h . r2 <= h . r1 )
assume ( r1 in dom h & r2 in dom h ) ; :: thesis: ( not r1 < r2 or h . r2 <= h . r1 )
then h . r1 = h . r2 by Z, FUNCT_1:def 16;
hence ( not r1 < r2 or h . r2 <= h . r1 ) ; :: thesis: verum

end;

let r1 be Element of REAL ; :: according to RFUNCT_2:def 4 :: thesis: for r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds
h . r1 <= h . r2
let r2 be Element of REAL ; :: thesis: ( r1 in dom h & r2 in dom h & r1 < r2 implies h . r1 <= h . r2 )
assume ( r1 in dom h & r2 in dom h ) ; :: thesis: ( not r1 < r2 or h . r1 <= h . r2 )
then h . r1 = h . r2 by Z, FUNCT_1:def 16;
hence ( not r1 < r2 or h . r1 <= h . r2 ) ; :: thesis: verum