A1: dom f = X by FUNCT_2:def 1;
thus ( f is bounded_below implies f .: X is bounded_below ) :: thesis: ( f .: X is bounded_below implies f is bounded_below )

proof

given r being Real such that A2: for y being object st y in dom f holds
r < f . y ; :: according to SEQ_2:def 2 :: thesis: f .: X is bounded_below
take r ; :: according to XXREAL_2:def 9 :: thesis: r is LowerBound of f .: X
let s be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not s in f .: X or r <= s )
assume s in f .: X ; :: thesis: r <= s
then ex x being object st
( x in X & x in X & s = f . x ) by FUNCT_2:64;
hence r <= s by A1, A2; :: thesis: verum

end;

given p being Real such that A3: p is LowerBound of f .: X ; :: according to XXREAL_2:def 9 :: thesis: f is bounded_below
take p - 1 ; :: according to SEQ_2:def 2 :: thesis: for b₁ being object holds
( not b₁ in dom f or not f . b₁ <= p - 1 )
let y be object ; :: thesis: ( not y in dom f or not f . y <= p - 1 )
assume y in dom f ; :: thesis: not f . y <= p - 1
then f . y in rng f by FUNCT_1:3;
then f . y in f .: X by RELSET_1:22;
then A4: p <= f . y by A3, XXREAL_2:def 2;
f . y < (f . y) + 1 by XREAL_1:29;
then p < (f . y) + 1 by A4, XXREAL_0:2;
hence not f . y <= p - 1 by XREAL_1:19; :: thesis: verum