let f be Function of R^1,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 ].((f . p) - s),((f . p) + s).[ c= f .: ].(p - r),(p + r).[ )
thus ( f is open implies for p being Point of R^1
for r being positive Real ex s being positive Real st ].((f . p) - s),((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 ].((f . p) - s),((f . p) + s).[ c= f .: ].(p - r),(p + r).[ ) implies f is open )

proof

assume A1: f is open ; :: thesis: for p being Point of R^1
for r being positive Real ex s being positive Real st ].((f . p) - s),((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 ].((f . p) - s),((f . p) + s).[ c= f .: ].(p - r),(p + r).[
let r be positive Real; :: thesis: ex s being positive Real st ].((f . p) - s),((f . p) + s).[ c= f .: ].(p - r),(p + r).[
reconsider p1 = p, q1 = f . p as Point of RealSpace ;
consider s being positive Real such that
A2: Ball (q1,s) c= f .: (Ball (p1,r)) by A1, Th6;
( ].(p - r),(p + r).[ = Ball (p1,r) & ].((f . p) - s),((f . p) + s).[ = Ball (q1,s) ) by FRECHET:7;
hence ex s being positive Real st ].((f . p) - s),((f . p) + s).[ c= f .: ].(p - r),(p + r).[ by A2; :: thesis: verum

end;

assume A3: for p being Point of R^1
for r being positive Real ex s being positive Real st ].((f . p) - s),((f . p) + s).[ c= f .: ].(p - r),(p + r).[ ; :: thesis: f is open
for p, q being Point of RealSpace
for r being positive Real st q = f . p holds
ex s being positive Real st Ball (q,s) c= f .: (Ball (p,r))

proof

let p, q be Point of RealSpace; :: thesis: for r being positive Real st q = f . p holds
ex s being positive Real st Ball (q,s) c= f .: (Ball (p,r))
let r be positive Real; :: thesis: ( q = f . p implies ex s being positive Real st Ball (q,s) c= f .: (Ball (p,r)) )
assume A4: q = f . p ; :: thesis: ex s being positive Real st Ball (q,s) c= f .: (Ball (p,r))
consider s being positive Real such that
A5: ].((f . p) - s),((f . p) + s).[ c= f .: ].(p - r),(p + r).[ by A3;
( ].(p - r),(p + r).[ = Ball (p,r) & ].((f . p) - s),((f . p) + s).[ = Ball (q,s) ) by A4, FRECHET:7;
hence ex s being positive Real st Ball (q,s) c= f .: (Ball (p,r)) by A5; :: thesis: verum

end;

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