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

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

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

assume f is constant ; :: thesis: f is bounded
reconsider z = 0 as real number ;
thus f is bounded_above :: according to SEQ_2:def 8 :: thesis: f is bounded_below

proof

take z ; :: according to SEQ_2:def 1 :: thesis: for b₁ being set holds
( not b₁ in dom f or not z <= f . b₁ )
let x be set ; :: thesis: ( not x in dom f or not z <= f . x )
thus ( not x in dom f or not z <= f . x ) by Z; :: thesis: verum

end;

take z ; :: according to SEQ_2:def 2 :: thesis: for b₁ being set holds
( not b₁ in dom f or not f . b₁ <= z )
let x be set ; :: thesis: ( not x in dom f or not f . x <= z )
thus ( not x in dom f or not f . x <= z ) by Z; :: thesis: verum

end;

suppose S: 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 number such that
W: for c being set st c in dom f holds
f . c = r by S, 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 1 :: thesis: for b₁ being set holds
( not b₁ in dom f or not r + 1 <= f . b₁ )
let y be set ; :: 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 W;
hence not r + 1 <= f . y by XREAL_1:41; :: thesis: verum

end;

take r - 1 ; :: according to SEQ_2:def 2 :: thesis: for b₁ being set holds
( not b₁ in dom f or not f . b₁ <= r - 1 )
let y be set ; :: 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 W;
hence not f . y <= r - 1 by XREAL_1:233; :: thesis: verum

end;

end;