let E, F be non trivial RealBanachSpace; :: thesis:
let Z be Subset of E; :: thesis:
let f be PartFunc of E,F; :: thesis:
assume A1: ( Z is open & dom f = Z & f is_differentiable_on Z & f `| Z is_continuous_on Z ) ; :: thesis:
assume A2: for x being Point of E st x in Z holds
diff (f,x) is invertible ; :: thesis:
thus A3: 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)) ) :: thesis:

proof

let x be Point of E; :: thesis:
let r1 be Real; :: thesis:
assume A4: ( x in Z & 0 < r1 ) ; :: thesis:
f . x in rng f by A1, A4, FUNCT_1:3;
then reconsider y = f . x as Point of F ;
diff (f,x) is invertible by A2, A4;
then consider r2 being Real such that
A5: ( 0 < r2 & Ball (y,r2) c= f .: (Ball (x,r1)) ) by A1, A4, Th18;
take y ; :: thesis:
take r2 ; :: thesis:
thus ( y = f . x & 0 < r2 & Ball (y,r2) c= f .: (Ball (x,r1)) ) by A5; :: thesis:

end;

for y being Point of F st y in f .: Z holds
ex r being Real st
( 0 < r & Ball (y,r) c= f .: Z )

proof

let y be Point of F; :: thesis:
assume y in f .: Z ; :: thesis:
then consider x being object such that
A6: ( x in dom f & x in Z & y = f . x ) by FUNCT_1:def 6;
reconsider x = x as Point of E by A6;
consider r1 being Real such that
A7: ( 0 < r1 & Ball (x,r1) c= Z ) by A1, A6, NDIFF_8:20;
consider y1 being Point of F, r2 being Real such that
A8: ( y1 = f . x & 0 < r2 & Ball (y1,r2) c= f .: (Ball (x,r1)) ) by A3, A6, A7;
take r2 ; :: thesis:
thus 0 < r2 by A8; :: thesis:
f .: (Ball (x,r1)) c= f .: Z by A7, RELAT_1:123;
hence Ball (y,r2) c= f .: Z by A6, A8, XBOOLE_1:1; :: thesis:

end;

hence f .: Z is open by NDIFF_8:20; :: thesis: