let T be non empty TopSpace; :: thesis: for M being non empty MetrSpace
for f being Function of T,() holds
( f is open iff for p being Point of T
for V being open Subset of T
for q being Point of M st q = f . p & p in V holds
ex r being positive Real st Ball (q,r) c= f .: V )

let M be non empty MetrSpace; :: thesis: for f being Function of T,() holds
( f is open iff for p being Point of T
for V being open Subset of T
for q being Point of M st q = f . p & p in V holds
ex r being positive Real st Ball (q,r) c= f .: V )

let f be Function of T,(); :: thesis: ( f is open iff for p being Point of T
for V being open Subset of T
for q being Point of M st q = f . p & p in V holds
ex r being positive Real st Ball (q,r) c= f .: V )

thus ( f is open implies for p being Point of T
for V being open Subset of T
for q being Point of M st q = f . p & p in V holds
ex r being positive Real st Ball (q,r) c= f .: V ) :: thesis: ( ( for p being Point of T
for V being open Subset of T
for q being Point of M st q = f . p & p in V holds
ex r being positive Real st Ball (q,r) c= f .: V ) implies f is open )
proof
assume A1: f is open ; :: thesis: for p being Point of T
for V being open Subset of T
for q being Point of M st q = f . p & p in V holds
ex r being positive Real st Ball (q,r) c= f .: V

let p be Point of T; :: thesis: for V being open Subset of T
for q being Point of M st q = f . p & p in V holds
ex r being positive Real st Ball (q,r) c= f .: V

let V be open Subset of T; :: thesis: for q being Point of M st q = f . p & p in V holds
ex r being positive Real st Ball (q,r) c= f .: V

let q be Point of M; :: thesis: ( q = f . p & p in V implies ex r being positive Real st Ball (q,r) c= f .: V )
assume A2: q = f . p ; :: thesis: ( not p in V or ex r being positive Real st Ball (q,r) c= f .: V )
assume p in V ; :: thesis: ex r being positive Real st Ball (q,r) c= f .: V
then consider W being open Subset of () such that
A3: f . p in W and
A4: W c= f .: V by ;
ex r being Real st
( r > 0 & Ball (q,r) c= W ) by ;
hence ex r being positive Real st Ball (q,r) c= f .: V by ; :: thesis: verum
end;
assume A5: for p being Point of T
for V being open Subset of T
for q being Point of M st q = f . p & p in V holds
ex r being positive Real st Ball (q,r) c= f .: V ; :: thesis: f is open
for p being Point of T
for V being open Subset of T st p in V holds
ex W being open Subset of () st
( f . p in W & W c= f .: V )
proof
let p be Point of T; :: thesis: for V being open Subset of T st p in V holds
ex W being open Subset of () st
( f . p in W & W c= f .: V )

let V be open Subset of T; :: thesis: ( p in V implies ex W being open Subset of () st
( f . p in W & W c= f .: V ) )

reconsider q = f . p as Point of M ;
assume p in V ; :: thesis: ex W being open Subset of () st
( f . p in W & W c= f .: V )

then consider r being positive Real such that
A6: Ball (q,r) c= f .: V by A5;
reconsider W = Ball (q,r) as open Subset of () by TOPMETR:14;
take W ; :: thesis: ( f . p in W & W c= f .: V )
thus f . p in W by GOBOARD6:1; :: thesis: W c= f .: V
thus W c= f .: V by A6; :: thesis: verum
end;
hence f is open by Th3; :: thesis: verum