consider r1 being real number such that
A2: for c being set st c in dom f1 holds
abs (f1 . c) <= r1 by Th89;
consider r2 being real number such that
A3: for c being set st c in dom f2 holds
abs (f2 . c) <= r2 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 )
assume c in dom (f1 (#) f2) ; :: thesis: abs ((f1 (#) f2) . c) <= r
then c in (dom f1) /\ (dom f2) by VALUED_1:def 4;
then X: ( c in dom f1 & c in dom f2 ) by XBOOLE_0:def 4;
then A5: abs (f1 . c) <= r1 by A2;
A6: abs (f2 . c) <= r2 by X, A3;
A7: 0 <= abs (f1 . c) by COMPLEX1:132;
0 <= abs (f2 . c) by COMPLEX1:132;
then (abs (f1 . c)) * (abs (f2 . c)) <= r by A5, A6, A7, 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 f1 (#) f2 is real-valued bounded Function by Th89; :: thesis: verum