let X, Y be set ; for C being non empty set
for V being RealNormSpace
for f2 being PartFunc of C,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 ; for V being RealNormSpace
for f2 being PartFunc of C,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; for f2 being PartFunc of C,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,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 f1 be PartFunc of C,REAL; ( 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
; f1 (#) f2 is_bounded_on X /\ Y
consider r1 being Real such that
A3:
for c being object st c in X /\ (dom f1) holds
|.(f1 . c).| <= r1
by A1, RFUNCT_1:73;
consider r2 being Real such that
A4:
for c being Element of C st c in Y /\ (dom f2) holds
||.(f2 /. c).|| <= r2
by A2;
reconsider r1 = r1 as Real ;
hence
f1 (#) f2 is_bounded_on X /\ Y
; verum