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 b1 being object holds
( not b1 in dom f or not z <= f . b1 )
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 b1 being object holds
( not b1 in dom f or not f . b1 <= 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 b1 being object holds
( not b1 in dom f or not r + 1 <= f . b1 )
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 b1 being object holds
( not b1 in dom f or not f . b1 <= 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;