consider r2 being Real such that

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

f2 . c < r2 by SEQ_2:def 1;

consider r1 being Real such that

A2: for c being object st c in dom f1 holds

f1 . c < r1 by SEQ_2:def 1;

_{1} being real-valued Function st b_{1} = f1 + f2 holds

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

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

f2 . c < r2 by SEQ_2:def 1;

consider r1 being Real such that

A2: for c being object st c in dom f1 holds

f1 . c < r1 by SEQ_2:def 1;

now :: thesis: ex r being set st

for c being object st c in dom (f1 + f2) holds

(f1 + f2) . c < r

hence
for bfor c being object st c in dom (f1 + f2) holds

(f1 + f2) . c < r

take r = r1 + r2; :: thesis: for c being object st c in dom (f1 + f2) holds

(f1 + f2) . c < r

let c be object ; :: thesis: ( c in dom (f1 + f2) implies (f1 + f2) . c < r )

assume A3: c in dom (f1 + f2) ; :: thesis: (f1 + f2) . c < r

then A4: c in (dom f1) /\ (dom f2) by VALUED_1:def 1;

then c in dom f1 by XBOOLE_0:def 4;

then A5: f1 . c < r1 by A2;

c in dom f2 by A4, XBOOLE_0:def 4;

then (f1 . c) + (f2 . c) < r by A1, A5, XREAL_1:8;

hence (f1 + f2) . c < r by A3, VALUED_1:def 1; :: thesis: verum

end;(f1 + f2) . c < r

let c be object ; :: thesis: ( c in dom (f1 + f2) implies (f1 + f2) . c < r )

assume A3: c in dom (f1 + f2) ; :: thesis: (f1 + f2) . c < r

then A4: c in (dom f1) /\ (dom f2) by VALUED_1:def 1;

then c in dom f1 by XBOOLE_0:def 4;

then A5: f1 . c < r1 by A2;

c in dom f2 by A4, XBOOLE_0:def 4;

then (f1 . c) + (f2 . c) < r by A1, A5, XREAL_1:8;

hence (f1 + f2) . c < r by A3, VALUED_1:def 1; :: thesis: verum

b