let X be non empty set ; :: thesis: for f being PartFunc of X,REAL st f | X is bounded_below holds
rng f is bounded_below
let f be PartFunc of X,REAL ; :: thesis: ( f | X is bounded_below implies rng f is bounded_below )
assume A1: f | X is bounded_below ; :: thesis: rng f is bounded_below
consider a being real number such that
A2: for x1 being set st x1 in X /\ (dom f) holds
a <= f . x1 by A1, RFUNCT_1:88;
A3: X /\ (dom f) = dom f by XBOOLE_1:28;
for y being real number st y in rng f holds
a <= y

proof

let y be real number ; :: thesis: ( y in rng f implies a <= y )
assume y in rng f ; :: thesis: a <= y
then consider s being set such that
A4: ( s in dom f & y = f . s ) by FUNCT_1:def 5;
thus a <= y by A2, A3, A4; :: thesis: verum

end;

hence rng f is bounded_below by SEQ_4:def 2; :: thesis: verum