theorem Th7:
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
partdiff`1 (
f,
(z1 + z2))
= (partdiff`1 (f,z1)) + (partdiff`1 (f,z2)) ) & ( for
z being
Point of
[:E,F:] for
a being
Real holds
partdiff`1 (
f,
(a * z))
= a * (partdiff`1 (f,z)) ) & ( for
z1,
z2 being
Point of
[:E,F:] holds
partdiff`1 (
f,
(z1 - z2))
= (partdiff`1 (f,z1)) - (partdiff`1 (f,z2)) ) )