theorem Th15:
for
E,
F being non
trivial RealBanachSpace for
D being
Subset of
E for
f being
PartFunc of
E,
F for
f1 being
PartFunc of
[:E,F:],
F for
Z being
Subset of
[:E,F:] st
D is
open &
dom f = D &
D <> {} &
f is_differentiable_on D &
f `| D is_continuous_on D &
Z = [:D, the carrier of F:] &
dom f1 = Z & ( for
s being
Point of
E for
t being
Point of
F st
s in D holds
f1 . (
s,
t)
= (f /. s) - t ) holds
(
f1 is_differentiable_on Z &
f1 `| Z is_continuous_on Z & ( for
x being
Point of
E for
y being
Point of
F for
z being
Point of
[:E,F:] st
x in D &
z = [x,y] holds
ex
I being
Point of
(R_NormSpace_of_BoundedLinearOperators (F,F)) st
(
I = id the
carrier of
F &
partdiff`1 (
f1,
z)
= diff (
f,
x) &
partdiff`2 (
f1,
z)
= - I ) ) )