let m, n 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 real positive number ex s being real positive number 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 real positive number ex s being real positive number 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)) ;
A2: ( m in NAT & n 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 s being real positive number st Ball (f . p),s c= f .: (Ball p,r) ) :: thesis: ( ( for p being Point of (TOP-REAL m)
for r being real positive number ex s being real positive number st Ball (f . p),s c= f .: (Ball p,r) ) implies f is open )

proof

assume A3: f is open ; :: thesis: for p being Point of (TOP-REAL m)
for r being real positive number ex s being real positive number st Ball (f . p),s c= f .: (Ball p,r)
let p be Point of (TOP-REAL m); :: thesis: for r being real positive number ex s being real positive number st Ball (f . p),s c= f .: (Ball p,r)
let r be real positive number ; :: thesis: ex s being real positive number st Ball (f . p),s c= f .: (Ball p,r)
reconsider p1 = p as Point of (Euclid m) by EUCLID:71;
reconsider q1 = f . p as Point of (Euclid n) by EUCLID:71;
f1 is open by A1, A3, Th1;
then consider s being real positive number such that
A4: Ball q1,s c= f1 .: (Ball p1,r) by Th6;
( Ball p1,r = Ball p,r & Ball q1,s = Ball (f . p),s ) by A2, TOPREAL9:13;
hence ex s being real positive number st Ball (f . p),s c= f .: (Ball p,r) by A4; :: thesis: verum

end;

assume A5: for p being Point of (TOP-REAL m)
for r being real positive number ex s being real positive number 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 real positive number st q = f1 . p holds
ex s being real positive number st Ball q,s c= f1 .: (Ball p,r)

proof

let p be Point of (Euclid m); :: thesis: for q being Point of (Euclid n)
for r being real positive number st q = f1 . p holds
ex s being real positive number st Ball q,s c= f1 .: (Ball p,r)
let q be Point of (Euclid n); :: thesis: for r being real positive number st q = f1 . p holds
ex s being real positive number st Ball q,s c= f1 .: (Ball p,r)
let r be real positive number ; :: thesis: ( q = f1 . p implies ex s being real positive number st Ball q,s c= f1 .: (Ball p,r) )
assume A6: q = f1 . p ; :: thesis: ex s being real positive number st Ball q,s c= f1 .: (Ball p,r)
reconsider p1 = p as Point of (TOP-REAL m) by EUCLID:71;
reconsider q1 = q as Point of (TOP-REAL n) by EUCLID:71;
consider s being real positive number such that
A7: Ball q1,s c= f .: (Ball p1,r) by A5, A6;
( Ball p1,r = Ball p,r & Ball q1,s = Ball q,s ) by A2, TOPREAL9:13;
hence ex s being real positive number st Ball q,s c= f1 .: (Ball p,r) by A7; :: thesis: verum

end;

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