let f be real-valued Function; :: thesis: ( f is constant implies f is bounded )

per cases
( f is empty or not f is empty )
;

end;

suppose A1:
f is empty
; :: thesis: ( f is constant implies f is bounded )

reconsider z = 0 as Real ;

assume f is constant ; :: thesis: f is bounded

thus f is bounded_above :: according to SEQ_2:def 8 :: thesis: f is bounded_below_{1} being object holds

( not b_{1} in dom f or not f . b_{1} <= z )

let x be object ; :: thesis: ( not x in dom f or not f . x <= z )

thus ( not x in dom f or not f . x <= z ) by A1; :: thesis: verum

end;assume f is constant ; :: thesis: f is bounded

thus f is bounded_above :: according to SEQ_2:def 8 :: thesis: f is bounded_below

proof

take
z
; :: according to SEQ_2:def 2 :: thesis: for b
take
z
; :: according to SEQ_2:def 1 :: thesis: for b_{1} being object holds

( not b_{1} in dom f or not z <= f . b_{1} )

let x be object ; :: thesis: ( not x in dom f or not z <= f . x )

thus ( not x in dom f or not z <= f . x ) by A1; :: thesis: verum

end;( not b

let x be object ; :: thesis: ( not x in dom f or not z <= f . x )

thus ( not x in dom f or not z <= f . x ) by A1; :: thesis: verum

( not b

let x be object ; :: thesis: ( not x in dom f or not f . x <= z )

thus ( not x in dom f or not f . x <= z ) by A1; :: thesis: verum

suppose A2:
not f is empty
; :: thesis: ( f is constant implies f is bounded )

assume
f is constant
; :: thesis: f is bounded

then consider r being Real such that

A3: for c being object st c in dom f holds

f . c = r by A2, VALUED_0:15;

thus f is bounded_above :: according to SEQ_2:def 8 :: thesis: f is bounded_below_{1} being object holds

( not b_{1} in dom f or not f . b_{1} <= r - 1 )

let y be object ; :: thesis: ( not y in dom f or not f . y <= r - 1 )

assume y in dom f ; :: thesis: not f . y <= r - 1

then f . y = r by A3;

hence not f . y <= r - 1 by XREAL_1:231; :: thesis: verum

end;then consider r being Real such that

A3: for c being object st c in dom f holds

f . c = r by A2, VALUED_0:15;

thus f is bounded_above :: according to SEQ_2:def 8 :: thesis: f is bounded_below

proof

take
r - 1
; :: according to SEQ_2:def 2 :: thesis: for b
take
r + 1
; :: according to SEQ_2:def 1 :: thesis: for b_{1} being object holds

( not b_{1} in dom f or not r + 1 <= f . b_{1} )

let y be object ; :: thesis: ( not y in dom f or not r + 1 <= f . y )

assume y in dom f ; :: thesis: not r + 1 <= f . y

then f . y = r by A3;

hence not r + 1 <= f . y by XREAL_1:39; :: thesis: verum

end;( not b

let y be object ; :: thesis: ( not y in dom f or not r + 1 <= f . y )

assume y in dom f ; :: thesis: not r + 1 <= f . y

then f . y = r by A3;

hence not r + 1 <= f . y by XREAL_1:39; :: thesis: verum

( not b

let y be object ; :: thesis: ( not y in dom f or not f . y <= r - 1 )

assume y in dom f ; :: thesis: not f . y <= r - 1

then f . y = r by A3;

hence not f . y <= r - 1 by XREAL_1:231; :: thesis: verum