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))) ) )