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