let n, m be Nat; :: thesis: for f being Function of (TOP-REAL m),(TOP-REAL n) holds

( f is open iff for p being Point of (TOP-REAL m)

for r being positive Real ex s being positive Real st Ball ((f . p),s) c= f .: (Ball (p,r)) )

let f be Function of (TOP-REAL m),(TOP-REAL n); :: thesis: ( f is open iff for p being Point of (TOP-REAL m)

for r being positive Real ex s being positive Real st Ball ((f . p),s) c= f .: (Ball (p,r)) )

A1: ( TopStruct(# the U1 of (TOP-REAL m), the topology of (TOP-REAL m) #) = TopSpaceMetr (Euclid m) & TopStruct(# the U1 of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) ) by EUCLID:def 8;

then reconsider f1 = f as Function of (TopSpaceMetr (Euclid m)),(TopSpaceMetr (Euclid n)) ;

thus ( f is open implies for p being Point of (TOP-REAL m)

for r being positive Real ex s being positive Real st Ball ((f . p),s) c= f .: (Ball (p,r)) ) :: thesis: ( ( for p being Point of (TOP-REAL m)

for r being positive Real ex s being positive Real st Ball ((f . p),s) c= f .: (Ball (p,r)) ) implies f is open )

for r being positive Real ex s being positive Real st Ball ((f . p),s) c= f .: (Ball (p,r)) ; :: thesis: f is open

for p being Point of (Euclid m)

for q being Point of (Euclid n)

for r being positive Real st q = f1 . p holds

ex s being positive Real st Ball (q,s) c= f1 .: (Ball (p,r))

hence f is open by A1, Th1; :: thesis: verum

( f is open iff for p being Point of (TOP-REAL m)

for r being positive Real ex s being positive Real st Ball ((f . p),s) c= f .: (Ball (p,r)) )

let f be Function of (TOP-REAL m),(TOP-REAL n); :: thesis: ( f is open iff for p being Point of (TOP-REAL m)

for r being positive Real ex s being positive Real st Ball ((f . p),s) c= f .: (Ball (p,r)) )

A1: ( TopStruct(# the U1 of (TOP-REAL m), the topology of (TOP-REAL m) #) = TopSpaceMetr (Euclid m) & TopStruct(# the U1 of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) ) by EUCLID:def 8;

then reconsider f1 = f as Function of (TopSpaceMetr (Euclid m)),(TopSpaceMetr (Euclid n)) ;

thus ( f is open implies for p being Point of (TOP-REAL m)

for r being positive Real ex s being positive Real st Ball ((f . p),s) c= f .: (Ball (p,r)) ) :: thesis: ( ( for p being Point of (TOP-REAL m)

for r being positive Real ex s being positive Real st Ball ((f . p),s) c= f .: (Ball (p,r)) ) implies f is open )

proof

assume A4:
for p being Point of (TOP-REAL m)
assume A2:
f is open
; :: thesis: for p being Point of (TOP-REAL m)

for r being positive Real ex s being positive Real st Ball ((f . p),s) c= f .: (Ball (p,r))

let p be Point of (TOP-REAL m); :: thesis: for r being positive Real ex s being positive Real st Ball ((f . p),s) c= f .: (Ball (p,r))

let r be positive Real; :: thesis: ex s being positive Real st Ball ((f . p),s) c= f .: (Ball (p,r))

reconsider p1 = p as Point of (Euclid m) by EUCLID:67;

reconsider q1 = f . p as Point of (Euclid n) by EUCLID:67;

f1 is open by A1, A2, Th1;

then consider s being positive Real such that

A3: Ball (q1,s) c= f1 .: (Ball (p1,r)) by Th6;

( Ball (p1,r) = Ball (p,r) & Ball (q1,s) = Ball ((f . p),s) ) by TOPREAL9:13;

hence ex s being positive Real st Ball ((f . p),s) c= f .: (Ball (p,r)) by A3; :: thesis: verum

end;for r being positive Real ex s being positive Real st Ball ((f . p),s) c= f .: (Ball (p,r))

let p be Point of (TOP-REAL m); :: thesis: for r being positive Real ex s being positive Real st Ball ((f . p),s) c= f .: (Ball (p,r))

let r be positive Real; :: thesis: ex s being positive Real st Ball ((f . p),s) c= f .: (Ball (p,r))

reconsider p1 = p as Point of (Euclid m) by EUCLID:67;

reconsider q1 = f . p as Point of (Euclid n) by EUCLID:67;

f1 is open by A1, A2, Th1;

then consider s being positive Real such that

A3: Ball (q1,s) c= f1 .: (Ball (p1,r)) by Th6;

( Ball (p1,r) = Ball (p,r) & Ball (q1,s) = Ball ((f . p),s) ) by TOPREAL9:13;

hence ex s being positive Real st Ball ((f . p),s) c= f .: (Ball (p,r)) by A3; :: thesis: verum

for r being positive Real ex s being positive Real st Ball ((f . p),s) c= f .: (Ball (p,r)) ; :: thesis: f is open

for p being Point of (Euclid m)

for q being Point of (Euclid n)

for r being positive Real st q = f1 . p holds

ex s being positive Real st Ball (q,s) c= f1 .: (Ball (p,r))

proof

then
f1 is open
by Th6;
let p be Point of (Euclid m); :: thesis: for q being Point of (Euclid n)

for r being positive Real st q = f1 . p holds

ex s being positive Real st Ball (q,s) c= f1 .: (Ball (p,r))

let q be Point of (Euclid n); :: thesis: for r being positive Real st q = f1 . p holds

ex s being positive Real st Ball (q,s) c= f1 .: (Ball (p,r))

let r be positive Real; :: thesis: ( q = f1 . p implies ex s being positive Real st Ball (q,s) c= f1 .: (Ball (p,r)) )

assume A5: q = f1 . p ; :: thesis: ex s being positive Real st Ball (q,s) c= f1 .: (Ball (p,r))

reconsider p1 = p as Point of (TOP-REAL m) by EUCLID:67;

reconsider q1 = q as Point of (TOP-REAL n) by EUCLID:67;

consider s being positive Real such that

A6: Ball (q1,s) c= f .: (Ball (p1,r)) by A4, A5;

( Ball (p1,r) = Ball (p,r) & Ball (q1,s) = Ball (q,s) ) by TOPREAL9:13;

hence ex s being positive Real st Ball (q,s) c= f1 .: (Ball (p,r)) by A6; :: thesis: verum

end;for r being positive Real st q = f1 . p holds

ex s being positive Real st Ball (q,s) c= f1 .: (Ball (p,r))

let q be Point of (Euclid n); :: thesis: for r being positive Real st q = f1 . p holds

ex s being positive Real st Ball (q,s) c= f1 .: (Ball (p,r))

let r be positive Real; :: thesis: ( q = f1 . p implies ex s being positive Real st Ball (q,s) c= f1 .: (Ball (p,r)) )

assume A5: q = f1 . p ; :: thesis: ex s being positive Real st Ball (q,s) c= f1 .: (Ball (p,r))

reconsider p1 = p as Point of (TOP-REAL m) by EUCLID:67;

reconsider q1 = q as Point of (TOP-REAL n) by EUCLID:67;

consider s being positive Real such that

A6: Ball (q1,s) c= f .: (Ball (p1,r)) by A4, A5;

( Ball (p1,r) = Ball (p,r) & Ball (q1,s) = Ball (q,s) ) by TOPREAL9:13;

hence ex s being positive Real st Ball (q,s) c= f1 .: (Ball (p,r)) by A6; :: thesis: verum

hence f is open by A1, Th1; :: thesis: verum