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

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 )
assume A6: c in dom (r (#) f) ; :: thesis: (r (#) f) . c < p
then A5: c in dom f by VALUED_1:def 5;
- (abs r1) <= r1 by ABSVALUE:11;
then - (abs r1) <= f . c by A5, A2, XXREAL_0:2;
then r * (f . c) <= r * (- (abs r1)) by XREAL_1:67;
then (r (#) f) . c <= r * (- (abs r1)) by A6, VALUED_1:def 5;
hence (r (#) f) . c < p by XREAL_1:41; :: thesis: verum

end;

hence r (#) f is real-valued bounded_above Function by SEQ_2:def 1; :: thesis: verum