let h be PartFunc of REAL,REAL; :: thesis: ( h is constant implies ( h is non-increasing & h is non-decreasing ) )
assume A1: 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 )
hence ( not r1 < r2 or h . r2 <= h . r1 ) by A1, FUNCT_1:def 16; :: 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 )
hence ( not r1 < r2 or h . r1 <= h . r2 ) by A1, FUNCT_1:def 16; :: thesis: verum