theorem Th15:
for
E,
F,
G being
RealNormSpace for
f being
Lipschitzian BilinearOperator of
E,
F,
G holds
(
f `| ([#] [:E,F:]) is
Lipschitzian LinearOperator of
[:E,F:],
(R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)) &
f `| ([#] [:E,F:]) is_differentiable_on [#] [:E,F:] &
f `| ([#] [:E,F:]) is_continuous_on the
carrier of
[:E,F:] & ( for
z being
Point of
[:E,F:] holds
diff (
(f `| ([#] [:E,F:])),
z)
= f `| ([#] [:E,F:]) ) )