theorem Th60:
for
i being
Nat for
S,
E,
F being
RealNormSpace for
u being
PartFunc of
S,
E for
v being
PartFunc of
S,
F for
w being
PartFunc of
S,
[:E,F:] for
Z being
Subset of
S st
w = <:u,v:> &
u is_differentiable_on i + 1,
Z &
v is_differentiable_on i + 1,
Z holds
(
w is_differentiable_on i + 1,
Z & ex
T being
Lipschitzian LinearOperator of
[:(diff_SP ((i + 1),S,E)),(diff_SP ((i + 1),S,F)):],
(diff_SP ((i + 1),S,[:E,F:])) st
diff (
w,
(i + 1),
Z)
= T * <:(diff (u,(i + 1),Z)),(diff (v,(i + 1),Z)):> )