consider r2 being real number such that
A1: for c being set st c in dom f2 holds
abs (f2 . c) <= r2 by Th89;
consider r1 being real number such that
A2: for c being set st c in dom f1 holds
abs (f1 . c) <= r1 by Th89;

now

take r = r1 * r2; :: thesis: for c being set st c in dom (f1 (#) f2) holds
abs ((f1 (#) f2) . c) <= r
let c be set ; :: thesis: ( c in dom (f1 (#) f2) implies abs ((f1 (#) f2) . c) <= r )
A3: 0 <= abs (f2 . c) by COMPLEX1:132;
assume c in dom (f1 (#) f2) ; :: thesis: abs ((f1 (#) f2) . c) <= r
then A4: c in (dom f1) /\ (dom f2) by VALUED_1:def 4;
then c in dom f1 by XBOOLE_0:def 4;
then A5: abs (f1 . c) <= r1 by A2;
c in dom f2 by A4, XBOOLE_0:def 4;
then A6: abs (f2 . c) <= r2 by A1;
0 <= abs (f1 . c) by COMPLEX1:132;
then (abs (f1 . c)) * (abs (f2 . c)) <= r by A5, A6, A3, XREAL_1:68;
then abs ((f1 . c) * (f2 . c)) <= r by COMPLEX1:151;
hence abs ((f1 (#) f2) . c) <= r by VALUED_1:5; :: thesis: verum

end;

hence for b₁ being real-valued Function st b₁ = f1 (#) f2 holds
b₁ is bounded by Th89; :: thesis: verum