let m be Nat; :: thesis: for f being Function of R^1,() holds
( f is open iff for p being Point of R^1
for r being positive Real ex s being positive Real st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[ )

let f be Function of R^1,(); :: thesis: ( f is open iff for p being Point of R^1
for r being positive Real ex s being positive Real st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[ )

A1: TopStruct(# the U1 of (), the topology of () #) = TopSpaceMetr () by EUCLID:def 8;
then reconsider f1 = f as Function of R^1,() ;
thus ( f is open implies for p being Point of R^1
for r being positive Real ex s being positive Real st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[ ) :: thesis: ( ( for p being Point of R^1
for r being positive Real ex s being positive Real st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[ ) implies f is open )
proof
assume A2: f is open ; :: thesis: for p being Point of R^1
for r being positive Real ex s being positive Real st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[

let p be Point of R^1; :: thesis: for r being positive Real ex s being positive Real st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[
let r be positive Real; :: thesis: ex s being positive Real st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[
reconsider p1 = p as Point of RealSpace ;
reconsider q1 = f . p as Point of () by EUCLID:67;
f1 is open by A1, A2, Th1;
then consider s being positive Real such that
A3: Ball (q1,s) c= f1 .: (Ball (p1,r)) by Th6;
( ].(p - r),(p + r).[ = Ball (p1,r) & Ball ((f . p),s) = Ball (q1,s) ) by ;
hence ex s being positive Real st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[ by A3; :: thesis: verum
end;
assume A4: for p being Point of R^1
for r being positive Real ex s being positive Real st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[ ; :: thesis: f is open
for p being Point of RealSpace
for q being Point of ()
for r being positive Real st q = f1 . p holds
ex s being positive Real st Ball (q,s) c= f1 .: (Ball (p,r))
proof
let p be Point of RealSpace; :: thesis: for q being Point of ()
for r being positive Real st q = f1 . p holds
ex s being positive Real st Ball (q,s) c= f1 .: (Ball (p,r))

let q be Point of (); :: thesis: for r being positive Real st q = f1 . p holds
ex s being positive Real st Ball (q,s) c= f1 .: (Ball (p,r))

let r be positive Real; :: thesis: ( q = f1 . p implies ex s being positive Real st Ball (q,s) c= f1 .: (Ball (p,r)) )
assume A5: q = f1 . p ; :: thesis: ex s being positive Real st Ball (q,s) c= f1 .: (Ball (p,r))
reconsider p1 = p as Point of R^1 ;
consider s being positive Real such that
A6: Ball ((f . p1),s) c= f .: ].(p1 - r),(p1 + r).[ by A4;
( ].(p1 - r),(p1 + r).[ = Ball (p,r) & Ball ((f . p1),s) = Ball (q,s) ) by ;
hence ex s being positive Real st Ball (q,s) c= f1 .: (Ball (p,r)) by A6; :: thesis: verum
end;
then f1 is open by Th6;
hence f is open by ; :: thesis: verum