theorem Th61:
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 for
i being
Nat st
w = <:u,v:> &
u is_differentiable_on i + 1,
Z &
diff (
u,
(i + 1),
Z)
is_continuous_on Z &
v is_differentiable_on i + 1,
Z &
diff (
v,
(i + 1),
Z)
is_continuous_on Z holds
(
w is_differentiable_on i + 1,
Z &
diff (
w,
(i + 1),
Z)
is_continuous_on Z )