let m be Nat; :: thesis: for f being Function of R^1 ,(TOP-REAL m) holds
( 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= Ball (f . p),r )
let f be Function of R^1 ,(TOP-REAL m); :: 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= Ball (f . p),r )
A1: TopStruct(# the U1 of (TOP-REAL m),the topology of (TOP-REAL m) #) = TopSpaceMetr (Euclid m) by EUCLID:def 8;
then reconsider f1 = f as Function of R^1 ,(TopSpaceMetr (Euclid m)) ;
A2: m in NAT by ORDINAL1:def 13;

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= Ball (f . p),r ) implies f is continuous )

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

end;

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

end;

then f1 is continuous by A1, Th17;
hence f is continuous by A1, YELLOW12:36; :: thesis: verum