theorem LmTh47:
for
X,
E,
G,
F being
RealNormSpace for
BL being
BilinearOperator of
E,
F,
G for
f being
PartFunc of
X,
E for
g being
PartFunc of
X,
F for
S being
Subset of
X st
BL is_continuous_on the
carrier of
[:E,F:] &
S c= dom f &
S c= dom g & ( for
s being
Point of
X st
s in S holds
f is_continuous_in s ) & ( for
s being
Point of
X st
s in S holds
g is_continuous_in s ) holds
ex
H being
PartFunc of
X,
G st
(
dom H = S & ( for
s being
Point of
X st
s in S holds
H . s = BL . (
(f . s),
(g . s)) ) &
H is_continuous_on S )