let M1, M2 be non empty MetrSpace; :: thesis: for f being Function of (TopSpaceMetr M1),(TopSpaceMetr M2) holds
( f is open iff for p being Point of M1
for q being Point of M2
for r being real positive number st q = f . p holds
ex s being real positive number st Ball q,s c= f .: (Ball p,r) )
let f be Function of (TopSpaceMetr M1),(TopSpaceMetr M2); :: thesis: ( f is open iff for p being Point of M1
for q being Point of M2
for r being real positive number st q = f . p holds
ex s being real positive number st Ball q,s c= f .: (Ball p,r) )
thus ( f is open implies for p being Point of M1
for q being Point of M2
for r being real positive number st q = f . p holds
ex s being real positive number st Ball q,s c= f .: (Ball p,r) ) :: thesis: ( ( for p being Point of M1
for q being Point of M2
for r being real positive number st q = f . p holds
ex s being real positive number st Ball q,s c= f .: (Ball p,r) ) implies f is open )

proof

assume A1: f is open ; :: thesis: for p being Point of M1
for q being Point of M2
for r being real positive number st q = f . p holds
ex s being real positive number st Ball q,s c= f .: (Ball p,r)
let p be Point of M1; :: thesis: for q being Point of M2
for r being real positive number st q = f . p holds
ex s being real positive number st Ball q,s c= f .: (Ball p,r)
let q be Point of M2; :: thesis: for r being real positive number st q = f . p holds
ex s being real positive number st Ball q,s c= f .: (Ball p,r)
let r be real positive number ; :: thesis: ( q = f . p implies ex s being real positive number st Ball q,s c= f .: (Ball p,r) )
assume A2: q = f . p ; :: thesis: ex s being real positive number st Ball q,s c= f .: (Ball p,r)
reconsider V = Ball p,r as Subset of (TopSpaceMetr M1) ;
A3: p in V by GOBOARD6:4;
V is open by TOPMETR:21;
hence ex s being real positive number st Ball q,s c= f .: (Ball p,r) by A1, A2, A3, Th4; :: thesis: verum

end;

assume A4: for p being Point of M1
for q being Point of M2
for r being real positive number st q = f . p holds
ex s being real positive number st Ball q,s c= f .: (Ball p,r) ; :: thesis: f is open
for p being Point of (TopSpaceMetr M1)
for V being open Subset of (TopSpaceMetr M1)
for q being Point of M2 st q = f . p & p in V holds
ex r being real positive number st Ball q,r c= f .: V

proof

let p be Point of (TopSpaceMetr M1); :: thesis: for V being open Subset of (TopSpaceMetr M1)
for q being Point of M2 st q = f . p & p in V holds
ex r being real positive number st Ball q,r c= f .: V
let V be open Subset of (TopSpaceMetr M1); :: thesis: for q being Point of M2 st q = f . p & p in V holds
ex r being real positive number st Ball q,r c= f .: V
let q be Point of M2; :: thesis: ( q = f . p & p in V implies ex r being real positive number st Ball q,r c= f .: V )
assume A5: q = f . p ; :: thesis: ( not p in V or ex r being real positive number st Ball q,r c= f .: V )
reconsider p1 = p as Point of M1 ;
assume p in V ; :: thesis: ex r being real positive number st Ball q,r c= f .: V
then consider r being real number such that
A6: r > 0 and
A7: Ball p1,r c= V by TOPMETR:22;
A8: f .: (Ball p1,r) c= f .: V by A7, RELAT_1:156;
ex s being real positive number st Ball q,s c= f .: (Ball p1,r) by A4, A5, A6;
hence ex r being real positive number st Ball q,r c= f .: V by A8, XBOOLE_1:1; :: thesis: verum

end;

hence f is open by Th4; :: thesis: verum