consider r1 being Real such that

A1: for c being object st c in dom f holds

f . c < r1 by SEQ_2:def 1;

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

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

A1: for c being object st c in dom f holds

f . c < r1 by SEQ_2:def 1;

now :: thesis: ex p being set st

for c being object st c in dom (r (#) f) holds

p < (r (#) f) . c

hence
for bfor c being object st c in dom (r (#) f) holds

p < (r (#) f) . c

take p = (r * |.r1.|) - 1; :: thesis: for c being object st c in dom (r (#) f) holds

p < (r (#) f) . c

let c be object ; :: thesis: ( c in dom (r (#) f) implies p < (r (#) f) . c )

A2: r1 <= |.r1.| by ABSVALUE:4;

assume A3: c in dom (r (#) f) ; :: thesis: p < (r (#) f) . c

then c in dom f by VALUED_1:def 5;

then f . c <= |.r1.| by A1, A2, XXREAL_0:2;

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

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

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

end;p < (r (#) f) . c

let c be object ; :: thesis: ( c in dom (r (#) f) implies p < (r (#) f) . c )

A2: r1 <= |.r1.| by ABSVALUE:4;

assume A3: c in dom (r (#) f) ; :: thesis: p < (r (#) f) . c

then c in dom f by VALUED_1:def 5;

then f . c <= |.r1.| by A1, A2, XXREAL_0:2;

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

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

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

b