consider r2 being Real such that
A1: for c being object st c in dom f2 holds
|.(f2 . c).| <= r2 by Th72;
consider r1 being Real such that
A2: for c being object st c in dom f1 holds
|.(f1 . c).| <= r1 by Th72;

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 )
A3: 0 <= |.(f2 . c).| by COMPLEX1:46;
assume c in dom (f1 (#) f2) ; :: thesis: |.((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: |.(f1 . c).| <= r1 by A2;
c in dom f2 by A4, XBOOLE_0:def 4;
then A6: |.(f2 . c).| <= r2 by A1;
0 <= |.(f1 . c).| by COMPLEX1:46;
then |.(f1 . c).| * |.(f2 . c).| <= r by A5, A6, A3, XREAL_1:66;
then |.((f1 . c) * (f2 . c)).| <= r by COMPLEX1:65;
hence |.((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 Th72; :: thesis: verum