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