theorem Th11:
for
E,
F,
G being
RealNormSpace for
f being
Lipschitzian BilinearOperator of
E,
F,
G ex
K being
Real st
(
0 <= K & ( for
z being
Point of
[:E,F:] holds
(
f is_differentiable_in z & ( for
dx being
Point of
E for
dy being
Point of
F holds
(diff (f,z)) . (
dx,
dy)
= (f . (dx,(z `2))) + (f . ((z `1),dy)) ) &
||.(diff (f,z)).|| <= K * ||.z.|| ) ) )