let E, F be non trivial RealBanachSpace; :: thesis: 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 )

let Z be Subset of E; :: thesis: 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 )

let f be PartFunc of E,F; :: thesis: ( 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 ) implies ( ( 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 ) )

assume A1: ( Z is open & dom f = Z & f is_differentiable_on Z & f `| Z is_continuous_on Z ) ; :: thesis: ( ex x being Point of E st
( x in Z & not diff (f,x) is invertible ) or ( ( 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 ) )

assume A2: for x being Point of E st x in Z holds
diff (f,x) is invertible ; :: thesis: ( ( 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 )

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: f .: Z is open
proof
let x be Point of E; :: thesis: 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)) )

let r1 be Real; :: thesis: ( x in Z & 0 < r1 implies ex y being Point of F ex r2 being Real st
( y = f . x & 0 < r2 & Ball (y,r2) c= f .: (Ball (x,r1)) ) )

assume A4: ( x in Z & 0 < r1 ) ; :: thesis: 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 . x in rng f by ;
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: ex r2 being Real st
( y = f . x & 0 < r2 & Ball (y,r2) c= f .: (Ball (x,r1)) )

take r2 ; :: thesis: ( y = f . x & 0 < r2 & Ball (y,r2) c= f .: (Ball (x,r1)) )
thus ( y = f . x & 0 < r2 & Ball (y,r2) c= f .: (Ball (x,r1)) ) by A5; :: thesis: verum
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: ( y in f .: Z implies ex r being Real st
( 0 < r & Ball (y,r) c= f .: Z ) )

assume y in f .: Z ; :: thesis: ex r being Real st
( 0 < r & Ball (y,r) c= f .: Z )

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 ;
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: ( 0 < r2 & Ball (y,r2) c= f .: Z )
thus 0 < r2 by A8; :: thesis: Ball (y,r2) c= f .: Z
f .: (Ball (x,r1)) c= f .: Z by ;
hence Ball (y,r2) c= f .: Z by ; :: thesis: verum
end;
hence f .: Z is open by NDIFF_8:20; :: thesis: verum