let f be real-valued Function; :: thesis: ( f is bounded_below implies rng f is bounded_below )
set X = dom f;
AA: f | (dom f) = f ;
assume f is bounded_below ; :: thesis: rng f is bounded_below
then consider a being Real such that
A1: for x1 being object st x1 in (dom f) /\ (dom f) holds
a <= f . x1 by AA, RFUNCT_1:71;
a is LowerBound of rng f
proof
let y be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not y in rng f or a <= y )
assume y in rng f ; :: thesis: a <= y
then ex s being object st
( s in dom f & y = f . s ) by FUNCT_1:def 3;
hence a <= y by A1; :: thesis: verum
end;
hence rng f is bounded_below ; :: thesis: verum