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

hereby :: thesis: ( ( for p being Point of R^1
for r being real positive number ex s being real positive number st f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[ ) implies f is continuous )

assume A1: f is continuous ; :: thesis: for p being Point of R^1
for r being real positive number ex s being real positive number st f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . 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),(p + s).[ c= ].((f . p) - r),((f . p) + r).[
let r be real positive number ; :: thesis: ex s being real positive number st f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[
reconsider p1 = p, q1 = f . p as Point of RealSpace ;
consider s being real positive number such that
A2: f .: (Ball p1,s) c= Ball q1,r by A1, Th17;
take s = s; :: thesis: f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[
( p1 in REAL & q1 in REAL & r in REAL & s in REAL ) by XREAL_0:def 1;
then ( Ball p1,s = ].(p1 - s),(p1 + s).[ & Ball q1,r = ].(q1 - r),(q1 + r).[ ) by FRECHET:7;
hence f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . 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),(p + s).[ c= ].((f . p) - r),((f . p) + r).[ ; :: thesis: f is continuous
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 f .: (Ball p,s) c= Ball q,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 f .: (Ball p,s) c= Ball q,r
let r be real positive number ; :: thesis: ( q = f . p implies ex s being real positive number st f .: (Ball p,s) c= Ball q,r )
assume A4: q = f . p ; :: thesis: ex s being real positive number st f .: (Ball p,s) c= Ball q,r
consider s being real positive number such that
A5: f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[ by A3;
take s ; :: thesis: f .: (Ball p,s) c= Ball q,r
( p in REAL & q in REAL & r in REAL & s in REAL ) by XREAL_0:def 1;
then ( Ball p,s = ].(p - s),(p + s).[ & Ball q,r = ].(q - r),(q + r).[ ) by FRECHET:7;
hence f .: (Ball p,s) c= Ball q,r by A5, A4; :: thesis: verum

end;

hence f is continuous by Th17; :: thesis: verum