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 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

proof

take z ; :: according to SEQ_2:def 1 :: thesis: for b₁ being object holds
( not b₁ in dom f or not z <= f . 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

end;

take z ; :: according to SEQ_2:def 2 :: thesis: for b₁ being object holds
( not b₁ in dom f or not f . b₁ <= 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;

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

proof

take r + 1 ; :: according to SEQ_2:def 1 :: thesis: for b₁ being object holds
( not b₁ in dom f or not r + 1 <= f . 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

end;

take r - 1 ; :: according to SEQ_2:def 2 :: thesis: for b₁ being object holds
( not b₁ in dom f or not f . b₁ <= 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;

end;