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;
now :: thesis: ex r being set st
for 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;
hence for b1 being real-valued Function st b1 = f1 + f2 holds
b1 is bounded_above ; :: thesis: verum