theorem Th34:
for
S,
E,
F,
G being
RealNormSpace 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 for
x being
Point of
S st
u is_differentiable_in x &
v is_differentiable_in x &
x in dom w &
W = B * w &
w = <:u,v:> holds
(
W is_differentiable_in x &
w is_differentiable_in x &
diff (
W,
x)
= (diff (B,[(u /. x),(v /. x)])) * (diff (w,x)) &
diff (
w,
x)
= <:(diff (u,x)),(diff (v,x)):> & ( for
ds being
Point of
S holds
(diff (W,x)) . ds = (B . (((diff (u,x)) . ds),(v /. x))) + (B . ((u /. x),((diff (v,x)) . ds))) ) )