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 )