consider r1 being real number such that
A1: 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
(r (#) f) . c < p
let c be set ; :: thesis: ( c in dom (r (#) f) implies (r (#) f) . c < p )
A2: r1 <= abs r1 by ABSVALUE:11;
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 < abs r1 by A1, A2, XXREAL_0:2;
then r * (f . c) <= (abs r1) * r by XREAL_1:66;
then (r (#) f) . c <= (abs r1) * r by A3, VALUED_1:def 5;
hence (r (#) f) . c < p by XREAL_1:41; :: thesis: verum

end;

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