let f be Function of R^1 ,R^1 ; :: thesis: ( f is open iff for p being Point of R^1
for r being real positive number ex s being real positive number 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 real positive number ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: ].(p - r),(p + r).[ ) :: thesis: ( ( for p being Point of R^1
for r being real positive number ex s being real positive number 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 real positive number ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: ].(p - r),(p + r).[
let p be Point of R^1 ; :: thesis: for r being real positive number ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: ].(p - r),(p + r).[
let r be real positive number ; :: thesis: ex s being real positive number 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 real positive number such that
A2: Ball q1,s c= f .: (Ball p1,r) by A1, Th6;
( r in REAL & s in REAL ) by XREAL_0:def 1;
then ( ].(p - r),(p + r).[ = Ball p1,r & ].((f . p) - s),((f . p) + s).[ = Ball q1,s ) by FRECHET:7;
hence ex s being real positive number 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 real positive number ex s being real positive number 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 real positive number st q = f . p holds
ex s being real positive number st Ball q,s c= f .: (Ball p,r)

proof

let p, q be Point of RealSpace ; :: 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 A4: q = f . p ; :: thesis: ex s being real positive number st Ball q,s c= f .: (Ball p,r)
consider s being real positive number such that
A5: ].((f . p) - s),((f . p) + s).[ c= f .: ].(p - r),(p + r).[ by A3;
( r in REAL & s in REAL ) by XREAL_0:def 1;
then ( ].(p - r),(p + r).[ = Ball p,r & ].((f . p) - s),((f . p) + s).[ = Ball q,s ) by A4, FRECHET:7;
hence ex s being real positive number st Ball q,s c= f .: (Ball p,r) by A5; :: thesis: verum

end;

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