let X, Y be set ; :: thesis: for C being non empty set
for V being RealNormSpace
for f2 being PartFunc of C,the carrier of V
for f1 being PartFunc of C,REAL st f1 | X is bounded & f2 is_bounded_on Y holds
f1 (#) f2 is_bounded_on X /\ Y
let C be non empty set ; :: thesis: for V being RealNormSpace
for f2 being PartFunc of C,the carrier of V
for f1 being PartFunc of C,REAL st f1 | X is bounded & f2 is_bounded_on Y holds
f1 (#) f2 is_bounded_on X /\ Y
let V be RealNormSpace; :: thesis: for f2 being PartFunc of C,the carrier of V
for f1 being PartFunc of C,REAL st f1 | X is bounded & f2 is_bounded_on Y holds
f1 (#) f2 is_bounded_on X /\ Y
let f2 be PartFunc of C,the carrier of V; :: thesis: for f1 being PartFunc of C,REAL st f1 | X is bounded & f2 is_bounded_on Y holds
f1 (#) f2 is_bounded_on X /\ Y
let f1 be PartFunc of C,REAL ; :: thesis: ( f1 | X is bounded & f2 is_bounded_on Y implies f1 (#) f2 is_bounded_on X /\ Y )
assume A1: ( f1 | X is bounded & f2 is_bounded_on Y ) ; :: thesis: f1 (#) f2 is_bounded_on X /\ Y
then consider r1 being real number such that
A2: for c being set st c in X /\ (dom f1) holds
abs (f1 . c) <= r1 by RFUNCT_1:90;
reconsider r1 = r1 as Real by XREAL_0:def 1;
consider r2 being Real such that
A3: for c being Element of C st c in Y /\ (dom f2) holds
||.(f2 /. c).|| <= r2 by A1, Def7;

now

take r = r1 * r2; :: thesis: for c being Element of C st c in (X /\ Y) /\ (dom (f1 (#) f2)) holds
||.((f1 (#) f2) /. c).|| <= r
let c be Element of C; :: thesis: ( c in (X /\ Y) /\ (dom (f1 (#) f2)) implies ||.((f1 (#) f2) /. c).|| <= r )
assume c in (X /\ Y) /\ (dom (f1 (#) f2)) ; :: thesis: ||.((f1 (#) f2) /. c).|| <= r
then A4: ( c in X /\ Y & c in dom (f1 (#) f2) ) by XBOOLE_0:def 4;
then A5: ( c in X & c in Y & c in (dom f1) /\ (dom f2) ) by Def3, XBOOLE_0:def 4;
then ( c in dom f1 & c in dom f2 ) by XBOOLE_0:def 4;
then A6: ( c in X /\ (dom f1) & c in Y /\ (dom f2) ) by A5, XBOOLE_0:def 4;
then A7: abs (f1 . c) <= r1 by A2;
A8: ||.(f2 /. c).|| <= r2 by A3, A6;
A9: 0 <= abs (f1 . c) by COMPLEX1:132;
0 <= ||.(f2 /. c).|| by NORMSP_1:8;
then (abs (f1 . c)) * ||.(f2 /. c).|| <= r by A7, A8, A9, XREAL_1:68;
then ||.((f1 . c) * (f2 /. c)).|| <= r by NORMSP_1:def 2;
hence ||.((f1 (#) f2) /. c).|| <= r by A4, Def3; :: thesis: verum

end;

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