theorem Th58:
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 Z &
v is_differentiable_on Z holds
(
diff (
w,
0,
Z)
is_differentiable_on Z & ex
T being
Lipschitzian LinearOperator of
[:(diff_SP (1,S,E)),(diff_SP (1,S,F)):],
(diff_SP (1,S,[:E,F:])) st
(
T = CTP (
S,
(diff_SP (0,S,E)),
(diff_SP (0,S,F))) &
diff (
w,1,
Z)
= T * <:(diff (u,1,Z)),(diff (v,1,Z)):> ) )