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 number ;
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 set holds
( not b₁ in proj1 f or not z <= K250(f,b₁) )
let x be set ; :: thesis: ( not x in proj1 f or not z <= K250(f,x) )
thus ( not x in proj1 f or not z <= K250(f,x) ) by A1; :: thesis: verum

end;

take z ; :: according to SEQ_2:def 2 :: thesis: for b₁ being set holds
( not b₁ in proj1 f or not K250(f,b₁) <= z )
let x be set ; :: thesis: ( not x in proj1 f or not K250(f,x) <= z )
thus ( not x in proj1 f or not K250(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 number such that
A3: for c being set 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 set holds
( not b₁ in proj1 f or not r + 1 <= K250(f,b₁) )
let y be set ; :: thesis: ( not y in proj1 f or not r + 1 <= K250(f,y) )
assume y in dom f ; :: thesis: not r + 1 <= K250(f,y)
then f . y = r by A3;
hence not r + 1 <= K250(f,y) by XREAL_1:39; :: thesis: verum

end;

take r - 1 ; :: according to SEQ_2:def 2 :: thesis: for b₁ being set holds
( not b₁ in proj1 f or not K250(f,b₁) <= r - 1 )
let y be set ; :: thesis: ( not y in proj1 f or not K250(f,y) <= r - 1 )
assume y in dom f ; :: thesis: not K250(f,y) <= r - 1
then f . y = r by A3;
hence not K250(f,y) <= r - 1 by XREAL_1:231; :: thesis: verum

end;

end;