theorem Th47:
for
E being
RealNormSpace for
G,
F being non
trivial RealBanachSpace for
Z being
Subset of
[:E,F:] for
f being
PartFunc of
[:E,F:],
G for
c being
Point of
G 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 &
f is_differentiable_on Z &
f `| Z is_continuous_on Z &
dom g = A &
rng g c= B &
g is_continuous_on A & ( for
x being
Point of
E st
x in A holds
f . (
x,
(g . x))
= c ) & ( for
x being
Point of
E for
z being
Point of
[:E,F:] st
x in A &
z = [x,(g . x)] holds
partdiff`2 (
f,
z) is
invertible ) holds
(
g is_differentiable_on A &
g `| A is_continuous_on A & ( for
x being
Point of
E for
z being
Point of
[:E,F:] st
x in A &
z = [x,(g . x)] holds
diff (
g,
x)
= - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) ) )