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 real positive number 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 real positive number 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 real positive number 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 #) ;
A3: m in NAT by ORDINAL1:def 13;
thus ( f is open implies for p being Point of (TOP-REAL m)
for r being real positive number 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 real positive number ex W being open Subset of T st
( f . p in W & W c= f .: (Ball p,r) ) ) implies f is open )

proof

assume A4: f is open ; :: thesis: for p being Point of (TOP-REAL m)
for r being real positive number 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 real positive number ex W being open Subset of T st
( f . p in W & W c= f .: (Ball p,r) )
let r be real positive number ; :: 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:71;
f1 is open by A4, A1, A2, Th1;
then consider W being open Subset of T such that
A5: ( f1 . p in W & W c= f1 .: (Ball q,r) ) by Th5;
Ball p,r = Ball q,r by A3, TOPREAL9:13;
hence ex W being open Subset of T st
( f . p in W & W c= f .: (Ball p,r) ) by A5; :: thesis: verum

end;

assume A6: for p being Point of (TOP-REAL m)
for r being real positive number 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 real positive number ex W being open Subset of T st
( f1 . p in W & W c= f1 .: (Ball p,r) )

proof

let p be Point of (Euclid m); :: thesis: for r being real positive number ex W being open Subset of T st
( f1 . p in W & W c= f1 .: (Ball p,r) )
let r be real positive number ; :: 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:71;
consider W being open Subset of T such that
A7: ( f . q in W & W c= f .: (Ball q,r) ) by A6;
Ball p,r = Ball q,r by A3, TOPREAL9:13;
hence ex W being open Subset of T st
( f1 . p in W & W c= f1 .: (Ball p,r) ) by A7; :: thesis: verum

end;

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