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;

_{1} being real-valued Function st b_{1} = r (#) f holds

b_{1} is bounded_above
; :: thesis: verum

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

hence
for bfor 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 - |.r1.| <= f . c by A1, A2, XXREAL_0:2;

then r * (f . c) <= r * (- |.r1.|) by XREAL_1:65;

then (r (#) f) . c <= r * (- |.r1.|) by A3, VALUED_1:def 5;

hence (r (#) f) . c < p by XREAL_1:39; :: thesis: verum

end;(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 - |.r1.| <= f . c by A1, A2, XXREAL_0:2;

then r * (f . c) <= r * (- |.r1.|) by XREAL_1:65;

then (r (#) f) . c <= r * (- |.r1.|) by A3, VALUED_1:def 5;

hence (r (#) f) . c < p by XREAL_1:39; :: thesis: verum

b