consider r1 being real number such that
A2: for c being set st c in dom f holds
f . c < r1 by SEQ_2:def 1;

now

take p = (r * (abs r1)) - 1; :: thesis: for c being set st c in dom (r (#) f) holds
p < (r (#) f) . c
let c be set ; :: thesis: ( c in dom (r (#) f) implies p < (r (#) f) . c )
assume A7: c in dom (r (#) f) ; :: thesis: p < (r (#) f) . c
then A5: c in dom f by VALUED_1:def 5;
r1 <= abs r1 by ABSVALUE:11;
then f . c <= abs r1 by A5, A2, XXREAL_0:2;
then r * (abs r1) <= r * (f . c) by XREAL_1:67;
then r * (abs r1) <= (r (#) f) . c by A7, VALUED_1:def 5;
hence p < (r (#) f) . c by XREAL_1:233; :: thesis: verum

end;

hence for b₁ being real-valued Function st b₁ = r (#) f holds
b₁ is bounded_below by SEQ_2:def 2; :: thesis: verum