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

proof

let m be Element of NAT ; :: according to SEQM_3:def 3 :: thesis: for n being Element of NAT st m in dom f & n in dom f & m <= n holds
f . m <= f . n
let n be Element of NAT ; :: thesis: ( m in dom f & n in dom f & m <= n implies f . m <= f . n )
assume ( m in dom f & n in dom f & m <= n ) ; :: thesis: f . m <= f . n
hence f . m <= f . n by A7, FUNCT_1:def 16; :: thesis: verum

end;

let m be Element of NAT ; :: according to SEQM_3:def 4 :: thesis: for n being Element of NAT st m in dom f & n in dom f & m <= n holds
f . m >= f . n
let n be Element of NAT ; :: thesis: ( m in dom f & n in dom f & m <= n implies f . m >= f . n )
assume ( m in dom f & n in dom f & m <= n ) ; :: thesis: f . m >= f . n
hence f . m >= f . n by A7, FUNCT_1:def 16; :: thesis: verum