consider r1 being Real such that
A1: for c being object st c in dom f holds
r1 < f . c by SEQ_2:def 2;

now :: thesis: ex p being set st
for c being object st c in dom (r (#) f) holds
(r (#) f) . c > p

take p = (r * (- |.r1.|)) - 1; :: thesis: for c being object st c in dom (r (#) f) holds
(r (#) f) . c > p
let c be object ; :: thesis: ( c in dom (r (#) f) implies (r (#) f) . c > p )
A2: - |.r1.| <= r1 by ABSVALUE:4;
assume A3: c in dom (r (#) f) ; :: thesis: (r (#) f) . c > p
then c in dom f by VALUED_1:def 5;
then f . c >= - |.r1.| by A1, A2, XXREAL_0:2;
then r * (f . c) >= (- |.r1.|) * r by XREAL_1:64;
then (r (#) f) . c >= (- |.r1.|) * r by A3, VALUED_1:def 5;
hence (r (#) f) . c > p by XREAL_1:231; :: thesis: verum

end;

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