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

ex r being Real st

( 0 < r & Ball (y,r) c= f .: Z )

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

for y being Point of F st y in f .: Z holds
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 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: 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;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 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: 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

ex r being Real st

( 0 < r & Ball (y,r) c= f .: Z )

proof

hence
f .: Z is open
by NDIFF_8:20; :: thesis: verum
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 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: ( 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 A7, RELAT_1:123;

hence Ball (y,r2) c= f .: Z by A6, A8, XBOOLE_1:1; :: thesis: verum

end;( 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 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: ( 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 A7, RELAT_1:123;

hence Ball (y,r2) c= f .: Z by A6, A8, XBOOLE_1:1; :: thesis: verum