let X, Y be RealNormSpace; :: thesis: for f being PartFunc of X,Y
for A being Subset of X
for B being Subset of Y st dom f = A & f is_continuous_on A & A is open & B is open holds
f " B is open
let f be PartFunc of X,Y; :: thesis: for A being Subset of X
for B being Subset of Y st dom f = A & f is_continuous_on A & A is open & B is open holds
f " B is open
let A be Subset of X; :: thesis: for B being Subset of Y st dom f = A & f is_continuous_on A & A is open & B is open holds
f " B is open
let B be Subset of Y; :: thesis: ( dom f = A & f is_continuous_on A & A is open & B is open implies f " B is open )
assume that
A1: dom f = A and
A2: f is_continuous_on A and
A3: A is open and
A4: B is open ; :: thesis: f " B is open
for a being Point of X st a in f " B holds
ex s being Real st
( s > 0 & Ball (a,s) c= f " B )

proof

let a be Point of X; :: thesis: ( a in f " B implies ex s being Real st
( s > 0 & Ball (a,s) c= f " B ) )
assume a in f " B ; :: thesis: ex s being Real st
( s > 0 & Ball (a,s) c= f " B )
then A6: ( a in dom f & f . a in B ) by FUNCT_1:def 7;
then f /. a in B by PARTFUN1:def 6;
then consider t being Real such that
A7: ( t > 0 & Ball ((f /. a),t) c= B ) by A4, NDIFF_8:20;
consider s0 being Real such that
A8: ( 0 < s0 & ( for a1 being Point of X st a1 in A & ||.(a1 - a).|| < s0 holds
||.((f /. a1) - (f /. a)).|| < t ) ) by A1, A2, A6, A7, NFCONT_1:19;
consider s1 being Real such that
A9: ( 0 < s1 & Ball (a,s1) c= A ) by A1, A3, A6, NDIFF_8:20;
set s = min (s0,s1);
A10: min (s0,s1) <= s0 by XXREAL_0:17;
A11: min (s0,s1) <= s1 by XXREAL_0:17;
take min (s0,s1) ; :: thesis: ( min (s0,s1) > 0 & Ball (a,(min (s0,s1))) c= f " B )
thus 0 < min (s0,s1) by A8, A9, XXREAL_0:15; :: thesis: Ball (a,(min (s0,s1))) c= f " B
for a1 being object st a1 in Ball (a,(min (s0,s1))) holds
a1 in f " B

proof

let a1 be object ; :: thesis: ( a1 in Ball (a,(min (s0,s1))) implies a1 in f " B )
assume A13: a1 in Ball (a,(min (s0,s1))) ; :: thesis: a1 in f " B
then reconsider a1 = a1 as Point of X ;
A14: a1 in Ball (a,s1) by A11, A13, NDIFF_8:15, TARSKI:def 3;
A15: a1 in Ball (a,s0) by A10, A13, NDIFF_8:15, TARSKI:def 3;
a1 in { x where x is Point of X : ||.(x - a).|| < s0 } by A15, NDIFF_8:17;
then ex x being Point of X st
( a1 = x & ||.(x - a).|| < s0 ) ;
then ||.((f /. a1) - (f /. a)).|| < t by A8, A9, A14;
then f /. a1 in { y where y is Point of Y : ||.(y - (f /. a)).|| < t } ;
then f /. a1 in Ball ((f /. a),t) by NDIFF_8:17;
then f . a1 in Ball ((f /. a),t) by A1, A9, A14, PARTFUN1:def 6;
hence a1 in f " B by A1, A7, A9, A14, FUNCT_1:def 7; :: thesis: verum

end;

hence Ball (a,(min (s0,s1))) c= f " B by TARSKI:def 3; :: thesis: verum

end;

hence f " B is open by NDIFF_8:20; :: thesis: verum