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;

_{1} being real-valued Function st b_{1} = f1 (#) f2 holds

b_{1} is bounded
by Th72; :: thesis: verum

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

hence
for bfor 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;|.((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

b