theorem Th49:
for
E,
F being
RealNormSpace for
Z being non
empty Subset of
E for
L1 being
PartFunc of
E,
F for
L0 being
Point of
F st
Z is
open &
L1 = Z --> L0 holds
for
i being
Nat holds
( ex
P being
Point of
(diff_SP (i,E,F)) st
diff (
L1,
i,
Z)
= Z --> P &
diff (
L1,
i,
Z)
is_differentiable_on Z &
(diff (L1,i,Z)) `| Z is_continuous_on Z )