theorem Th45:
for
E,
G,
F being
RealNormSpace for
Z being
Subset of
[:E,F:] for
f being
PartFunc of
[:E,F:],
G for
a being
Point of
E for
b being
Point of
F for
c being
Point of
G for
z being
Point of
[:E,F:] for
A being
Subset of
E for
B being
Subset of
F for
g being
PartFunc of
E,
F st
Z is
open &
dom f = Z &
A is
open &
B is
open &
[:A,B:] c= Z &
z = [a,b] &
f . (
a,
b)
= c &
f is_differentiable_in z &
dom g = A &
rng g c= B &
a in A &
g . a = b &
g is_continuous_in a & ( for
x being
Point of
E st
x in A holds
f . (
x,
(g . x))
= c ) &
partdiff`2 (
f,
z) is
invertible holds
(
g is_differentiable_in a &
diff (
g,
a)
= - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) )