theorem Th10:
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:] ex
L being
Lipschitzian LinearOperator of
[:E,F:],
G st
( ( for
dx being
Point of
E for
dy being
Point of
F holds
L . (
dx,
dy)
= (f . (dx,(z `2))) + (f . ((z `1),dy)) ) & ( for
s being
Point of
[:E,F:] holds
||.(L . s).|| <= (K * ||.z.||) * ||.s.|| ) ) ) )