theorem Th65:
for
E being
RealBanachSpace for
F,
G being non
trivial RealBanachSpace for
Z being non
empty Subset of
[:E,F:] for
c being
Point of
G for
A being
Subset of
E for
B being
Subset of
F st
Z is
open &
A is
open &
B is
open &
[:A,B:] c= Z holds
for
i being
Nat for
f being
PartFunc of
[:E,F:],
G for
g being
PartFunc of
E,
F st
dom f = Z &
f is_differentiable_on i + 1,
Z &
diff (
f,
(i + 1),
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 i + 1,
A &
diff (
g,
(i + 1),
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))) ) )