let f be Function of R^1,R^1; :: thesis: ( f is continuous iff for p being Point of R^1
for r being positive Real ex s being positive Real 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 positive Real ex s being positive Real 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 positive Real ex s being positive Real st f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[
let p be Point of R^1; :: thesis: for r being positive Real ex s being positive Real st f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[
let r be positive Real; :: thesis: ex s being positive Real 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 positive Real 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).[
( 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 positive Real ex s being positive Real 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 positive Real st q = f . p holds
ex s being positive Real st f .: (Ball (p,s)) c= Ball (q,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 f .: (Ball (p,s)) c= Ball (q,r)
let r be positive Real; :: thesis: ( q = f . p implies ex s being positive Real st f .: (Ball (p,s)) c= Ball (q,r) )
assume A4: q = f . p ; :: thesis: ex s being positive Real st f .: (Ball (p,s)) c= Ball (q,r)
consider s being positive Real 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)
( 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