let M be non empty set ; :: thesis: for V being ComplexNormSpace
for f2 being PartFunc of M,V
for X, Y being set
for f1 being PartFunc of M,COMPLEX st f1 | X is bounded & f2 is_bounded_on Y holds
f1 (#) f2 is_bounded_on X /\ Y
let V be ComplexNormSpace; :: thesis: for f2 being PartFunc of M,V
for X, Y being set
for f1 being PartFunc of M,COMPLEX st f1 | X is bounded & f2 is_bounded_on Y holds
f1 (#) f2 is_bounded_on X /\ Y
let f2 be PartFunc of M,V; :: thesis: for X, Y being set
for f1 being PartFunc of M,COMPLEX st f1 | X is bounded & f2 is_bounded_on Y holds
f1 (#) f2 is_bounded_on X /\ Y
let X, Y be set ; :: thesis: for f1 being PartFunc of M,COMPLEX st f1 | X is bounded & f2 is_bounded_on Y holds
f1 (#) f2 is_bounded_on X /\ Y
let f1 be PartFunc of M,COMPLEX; :: thesis: ( f1 | X is bounded & f2 is_bounded_on Y implies f1 (#) f2 is_bounded_on X /\ Y )
assume that
A1: f1 | X is bounded and
A2: f2 is_bounded_on Y ; :: thesis: f1 (#) f2 is_bounded_on X /\ Y
consider r1 being Real such that
A3: for c being Element of M st c in X /\ (dom f1) holds
|.(f1 /. c).| <= r1 by A1, CFUNCT_1:69;
consider r2 being Real such that
A4: for c being Element of M st c in Y /\ (dom f2) holds
||.(f2 /. c).|| <= r2 by A2;
reconsider r1 = r1 as Real ;

now :: thesis: ex r being set st
for c being Element of M st c in (X /\ Y) /\ (dom (f1 (#) f2)) holds
||.((f1 (#) f2) /. c).|| <= r

take r = r1 * r2; :: thesis: for c being Element of M st c in (X /\ Y) /\ (dom (f1 (#) f2)) holds
||.((f1 (#) f2) /. c).|| <= r
let c be Element of M; :: thesis: ( c in (X /\ Y) /\ (dom (f1 (#) f2)) implies ||.((f1 (#) f2) /. c).|| <= r )
assume A5: c in (X /\ Y) /\ (dom (f1 (#) f2)) ; :: thesis: ||.((f1 (#) f2) /. c).|| <= r
then A6: c in X /\ Y by XBOOLE_0:def 4;
then A7: c in X by XBOOLE_0:def 4;
A8: c in dom (f1 (#) f2) by A5, XBOOLE_0:def 4;
then A9: c in (dom f1) /\ (dom f2) by Def1;
then c in dom f1 by XBOOLE_0:def 4;
then c in X /\ (dom f1) by A7, XBOOLE_0:def 4;
then A10: |.(f1 /. c).| <= r1 by A3;
A11: c in Y by A6, XBOOLE_0:def 4;
c in dom f2 by A9, XBOOLE_0:def 4;
then c in Y /\ (dom f2) by A11, XBOOLE_0:def 4;
then A12: ||.(f2 /. c).|| <= r2 by A4;
( 0 <= |.(f1 /. c).| & 0 <= ||.(f2 /. c).|| ) by CLVECT_1:105, COMPLEX1:46;
then |.(f1 /. c).| * ||.(f2 /. c).|| <= r by A10, A12, XREAL_1:66;
then ||.((f1 /. c) * (f2 /. c)).|| <= r by CLVECT_1:def 13;
hence ||.((f1 (#) f2) /. c).|| <= r by A8, Def1; :: thesis: verum

end;

hence f1 (#) f2 is_bounded_on X /\ Y ; :: thesis: verum