consider r1 being real number such that
A3: for c being set st c in dom f1 holds
f1 . c < r1 by SEQ_2:def 1;
consider r2 being real number such that
A4: for c being set st c in dom f2 holds
f2 . c < r2 by SEQ_2:def 1;

now

take r = r1 + r2; :: thesis: for c being set st c in dom (f1 + f2) holds
(f1 + f2) . c < r
let c be set ; :: thesis: ( c in dom (f1 + f2) implies (f1 + f2) . c < r )
assume A5: c in dom (f1 + f2) ; :: thesis: (f1 + f2) . c < r
then c in (dom f1) /\ (dom f2) by VALUED_1:def 1;
then A6: ( c in dom f1 & c in dom f2 ) by XBOOLE_0:def 4;
then f1 . c < r1 by A3;
then (f1 . c) + (f2 . c) < r by A4, A6, XREAL_1:10;
hence (f1 + f2) . c < r by A5, VALUED_1:def 1; :: thesis: verum

end;

hence for b₁ being real-valued Function st b₁ = f1 + f2 holds
b₁ is bounded_above by SEQ_2:def 1; :: thesis: verum