for E, F being non trivial RealBanachSpace
for Z being Subset of E
for f being PartFunc of E,F st Z is open & dom f = Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & ( for x being Point of E st x in Z holds
diff (f,x) is invertible ) holds
( ( for x being Point of E
for r1 being Real st x in Z & 0 < r1 holds
ex y being Point of F ex r2 being Real st
( y = f . x & 0 < r2 & Ball (y,r2) c= f .: (Ball (x,r1)) ) ) & f .: Z is open )