let m be Nat; :: thesis: for T being non empty TopSpace

for f being Function of (TOP-REAL m),T holds

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

for r being positive Real ex W being open Subset of T st

( f . p in W & W c= f .: (Ball (p,r)) ) )

let T be non empty TopSpace; :: thesis: for f being Function of (TOP-REAL m),T holds

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

for r being positive Real ex W being open Subset of T st

( f . p in W & W c= f .: (Ball (p,r)) ) )

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

for r being positive Real ex W being open Subset of T st

( f . p in W & W c= f .: (Ball (p,r)) ) )

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

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

A2: TopStruct(# the U1 of T, the topology of T #) = TopStruct(# the U1 of T, the topology of T #) ;

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

for r being positive Real ex W being open Subset of T st

( f . p in W & W c= f .: (Ball (p,r)) ) ) :: thesis: ( ( for p being Point of (TOP-REAL m)

for r being positive Real ex W being open Subset of T st

( f . p in W & W c= f .: (Ball (p,r)) ) ) implies f is open )

for r being positive Real ex W being open Subset of T st

( f . p in W & W c= f .: (Ball (p,r)) ) ; :: thesis: f is open

for p being Point of (Euclid m)

for r being positive Real ex W being open Subset of T st

( f1 . p in W & W c= f1 .: (Ball (p,r)) )

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

for f being Function of (TOP-REAL m),T holds

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

for r being positive Real ex W being open Subset of T st

( f . p in W & W c= f .: (Ball (p,r)) ) )

let T be non empty TopSpace; :: thesis: for f being Function of (TOP-REAL m),T holds

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

for r being positive Real ex W being open Subset of T st

( f . p in W & W c= f .: (Ball (p,r)) ) )

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

for r being positive Real ex W being open Subset of T st

( f . p in W & W c= f .: (Ball (p,r)) ) )

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

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

A2: TopStruct(# the U1 of T, the topology of T #) = TopStruct(# the U1 of T, the topology of T #) ;

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

for r being positive Real ex W being open Subset of T st

( f . p in W & W c= f .: (Ball (p,r)) ) ) :: thesis: ( ( for p being Point of (TOP-REAL m)

for r being positive Real ex W being open Subset of T st

( f . p in W & W c= f .: (Ball (p,r)) ) ) implies f is open )

proof

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

for r being positive Real ex W being open Subset of T st

( f . p in W & W c= f .: (Ball (p,r)) )

let p be Point of (TOP-REAL m); :: thesis: for r being positive Real ex W being open Subset of T st

( f . p in W & W c= f .: (Ball (p,r)) )

let r be positive Real; :: thesis: ex W being open Subset of T st

( f . p in W & W c= f .: (Ball (p,r)) )

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

f1 is open by A3, A1, A2, Th1;

then consider W being open Subset of T such that

A4: ( f1 . p in W & W c= f1 .: (Ball (q,r)) ) by Th5;

Ball (p,r) = Ball (q,r) by TOPREAL9:13;

hence ex W being open Subset of T st

( f . p in W & W c= f .: (Ball (p,r)) ) by A4; :: thesis: verum

end;for r being positive Real ex W being open Subset of T st

( f . p in W & W c= f .: (Ball (p,r)) )

let p be Point of (TOP-REAL m); :: thesis: for r being positive Real ex W being open Subset of T st

( f . p in W & W c= f .: (Ball (p,r)) )

let r be positive Real; :: thesis: ex W being open Subset of T st

( f . p in W & W c= f .: (Ball (p,r)) )

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

f1 is open by A3, A1, A2, Th1;

then consider W being open Subset of T such that

A4: ( f1 . p in W & W c= f1 .: (Ball (q,r)) ) by Th5;

Ball (p,r) = Ball (q,r) by TOPREAL9:13;

hence ex W being open Subset of T st

( f . p in W & W c= f .: (Ball (p,r)) ) by A4; :: thesis: verum

for r being positive Real ex W being open Subset of T st

( f . p in W & W c= f .: (Ball (p,r)) ) ; :: thesis: f is open

for p being Point of (Euclid m)

for r being positive Real ex W being open Subset of T st

( f1 . p in W & W c= f1 .: (Ball (p,r)) )

proof

then
f1 is open
by Th5;
let p be Point of (Euclid m); :: thesis: for r being positive Real ex W being open Subset of T st

( f1 . p in W & W c= f1 .: (Ball (p,r)) )

let r be positive Real; :: thesis: ex W being open Subset of T st

( f1 . p in W & W c= f1 .: (Ball (p,r)) )

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

consider W being open Subset of T such that

A6: ( f . q in W & W c= f .: (Ball (q,r)) ) by A5;

Ball (p,r) = Ball (q,r) by TOPREAL9:13;

hence ex W being open Subset of T st

( f1 . p in W & W c= f1 .: (Ball (p,r)) ) by A6; :: thesis: verum

end;( f1 . p in W & W c= f1 .: (Ball (p,r)) )

let r be positive Real; :: thesis: ex W being open Subset of T st

( f1 . p in W & W c= f1 .: (Ball (p,r)) )

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

consider W being open Subset of T such that

A6: ( f . q in W & W c= f .: (Ball (q,r)) ) by A5;

Ball (p,r) = Ball (q,r) by TOPREAL9:13;

hence ex W being open Subset of T st

( f1 . p in W & W c= f1 .: (Ball (p,r)) ) by A6; :: thesis: verum

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