theorem Th35:
for
S,
E,
F,
G being
RealNormSpace for
Z being
Subset of
S for
B being
Lipschitzian BilinearOperator of
E,
F,
G for
W being
PartFunc of
S,
G for
w being
PartFunc of
S,
[:E,F:] for
u being
PartFunc of
S,
E for
v being
PartFunc of
S,
F st
u is_differentiable_on Z &
v is_differentiable_on Z &
W = B * w &
w = <:u,v:> holds
(
W is_differentiable_on Z & ( for
x being
Point of
S st
x in Z holds
for
ds being
Point of
S holds
((W `| Z) /. x) . ds = (B . ((((u `| Z) /. x) . ds),(v /. x))) + (B . ((u /. x),(((v `| Z) /. x) . ds))) ) )