theorem Th13:
for
E,
F,
G being
RealNormSpace for
f being
Lipschitzian BilinearOperator of
E,
F,
G holds
( ( for
z1,
z2 being
Point of
[:E,F:] holds
diff (
f,
(z1 + z2))
= (diff (f,z1)) + (diff (f,z2)) ) & ( for
z being
Point of
[:E,F:] for
a being
Real holds
diff (
f,
(a * z))
= a * (diff (f,z)) ) & ( for
z1,
z2 being
Point of
[:E,F:] holds
diff (
f,
(z1 - z2))
= (diff (f,z1)) - (diff (f,z2)) ) )