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