theorem Th5:
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
r1,
r2 being
Real for
g being
PartFunc of
E,
F for
P being
Lipschitzian LinearOperator of
E,
G for
Q being
Lipschitzian LinearOperator of
G,
F st
Z is
open &
dom f = Z &
z = [a,b] &
z in Z &
f . (
a,
b)
= c &
f is_differentiable_in z &
0 < r1 &
0 < r2 &
dom g = Ball (
a,
r1) &
rng g c= Ball (
b,
r2) &
g . a = b &
g is_continuous_in a & ( for
x being
Point of
E st
x in Ball (
a,
r1) holds
f . (
x,
(g . x))
= c ) &
partdiff`2 (
f,
z) is
one-to-one &
Q = (partdiff`2 (f,z)) " &
P = partdiff`1 (
f,
z) holds
(
g is_differentiable_in a &
diff (
g,
a)
= - (Q * P) )