theorem Th53:
for
i being
Nat for
E,
F,
G being
RealNormSpace for
Z being non
empty Subset of
[:E,F:] for
f being
PartFunc of
[:E,F:],
G st
f is_differentiable_on i + 1,
Z &
diff (
f,
(i + 1),
Z)
is_continuous_on Z holds
(
f `partial`1| Z is_differentiable_on i,
Z &
diff (
(f `partial`1| Z),
i,
Z)
is_continuous_on Z &
f `partial`2| Z is_differentiable_on i,
Z &
diff (
(f `partial`2| Z),
i,
Z)
is_continuous_on Z )