let m be Nat; :: thesis: for f being Function of (TOP-REAL m),R^1 holds

( f is continuous iff for p being Point of (TOP-REAL m)

for r being positive Real ex s being positive Real st f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[ )

let f be Function of (TOP-REAL m),R^1; :: thesis: ( f is continuous iff for p being Point of (TOP-REAL m)

for r being positive Real ex s being positive Real st f .: (Ball (p,s)) c= ].((f . p) - r),((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 (TopSpaceMetr (Euclid m)),R^1 ;

for r being positive Real ex s being positive Real st f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[ ; :: thesis: f is continuous

for p being Point of (Euclid m)

for q being Point of RealSpace

for r being positive Real st q = f1 . p holds

ex s being positive Real st f1 .: (Ball (p,s)) c= Ball (q,r)

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

( f is continuous iff for p being Point of (TOP-REAL m)

for r being positive Real ex s being positive Real st f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[ )

let f be Function of (TOP-REAL m),R^1; :: thesis: ( f is continuous iff for p being Point of (TOP-REAL m)

for r being positive Real ex s being positive Real st f .: (Ball (p,s)) c= ].((f . p) - r),((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 (TopSpaceMetr (Euclid m)),R^1 ;

hereby :: thesis: ( ( for p being Point of (TOP-REAL m)

for r being positive Real ex s being positive Real st f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[ ) implies f is continuous )

assume A4:
for p being Point of (TOP-REAL m)for r being positive Real ex s being positive Real st f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[ ) implies f is continuous )

assume A2:
f is continuous
; :: thesis: for p being Point of (TOP-REAL m)

for r being positive Real ex s being positive Real st f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[

let p be Point of (TOP-REAL m); :: thesis: for r being positive Real ex s being positive Real st f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[

let r be positive Real; :: thesis: ex s being positive Real st f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[

reconsider p1 = p as Point of (Euclid m) by EUCLID:67;

reconsider q1 = f . p as Point of RealSpace ;

f1 is continuous by A1, A2, YELLOW12:36;

then consider s being positive Real such that

A3: f .: (Ball (p1,s)) c= Ball (q1,r) by A1, Th17;

take s = s; :: thesis: f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[

( Ball (p1,s) = Ball (p,s) & Ball (q1,r) = ].((f . p) - r),((f . p) + r).[ ) by FRECHET:7, TOPREAL9:13;

hence f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[ by A3; :: thesis: verum

end;for r being positive Real ex s being positive Real st f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[

let p be Point of (TOP-REAL m); :: thesis: for r being positive Real ex s being positive Real st f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[

let r be positive Real; :: thesis: ex s being positive Real st f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[

reconsider p1 = p as Point of (Euclid m) by EUCLID:67;

reconsider q1 = f . p as Point of RealSpace ;

f1 is continuous by A1, A2, YELLOW12:36;

then consider s being positive Real such that

A3: f .: (Ball (p1,s)) c= Ball (q1,r) by A1, Th17;

take s = s; :: thesis: f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[

( Ball (p1,s) = Ball (p,s) & Ball (q1,r) = ].((f . p) - r),((f . p) + r).[ ) by FRECHET:7, TOPREAL9:13;

hence f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[ by A3; :: thesis: verum

for r being positive Real ex s being positive Real st f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[ ; :: thesis: f is continuous

for p being Point of (Euclid m)

for q being Point of RealSpace

for r being positive Real st q = f1 . p holds

ex s being positive Real st f1 .: (Ball (p,s)) c= Ball (q,r)

proof

then
f1 is continuous
by Th17;
let p be Point of (Euclid m); :: thesis: for q being Point of RealSpace

for r being positive Real st q = f1 . p holds

ex s being positive Real st f1 .: (Ball (p,s)) c= Ball (q,r)

let q be Point of RealSpace; :: thesis: for r being positive Real st q = f1 . p holds

ex s being positive Real st f1 .: (Ball (p,s)) c= Ball (q,r)

let r be positive Real; :: thesis: ( q = f1 . p implies ex s being positive Real st f1 .: (Ball (p,s)) c= Ball (q,r) )

assume A5: q = f1 . p ; :: thesis: ex s being positive Real st f1 .: (Ball (p,s)) c= Ball (q,r)

reconsider p1 = p as Point of (TOP-REAL m) by EUCLID:67;

consider s being positive Real such that

A6: f .: (Ball (p1,s)) c= ].((f . p) - r),((f . p) + r).[ by A4;

take s ; :: thesis: f1 .: (Ball (p,s)) c= Ball (q,r)

( Ball (p1,s) = Ball (p,s) & ].((f . p) - r),((f . p) + r).[ = Ball (q,r) ) by A5, FRECHET:7, TOPREAL9:13;

hence f1 .: (Ball (p,s)) c= Ball (q,r) by A6; :: thesis: verum

end;for r being positive Real st q = f1 . p holds

ex s being positive Real st f1 .: (Ball (p,s)) c= Ball (q,r)

let q be Point of RealSpace; :: thesis: for r being positive Real st q = f1 . p holds

ex s being positive Real st f1 .: (Ball (p,s)) c= Ball (q,r)

let r be positive Real; :: thesis: ( q = f1 . p implies ex s being positive Real st f1 .: (Ball (p,s)) c= Ball (q,r) )

assume A5: q = f1 . p ; :: thesis: ex s being positive Real st f1 .: (Ball (p,s)) c= Ball (q,r)

reconsider p1 = p as Point of (TOP-REAL m) by EUCLID:67;

consider s being positive Real such that

A6: f .: (Ball (p1,s)) c= ].((f . p) - r),((f . p) + r).[ by A4;

take s ; :: thesis: f1 .: (Ball (p,s)) c= Ball (q,r)

( Ball (p1,s) = Ball (p,s) & ].((f . p) - r),((f . p) + r).[ = Ball (q,r) ) by A5, FRECHET:7, TOPREAL9:13;

hence f1 .: (Ball (p,s)) c= Ball (q,r) by A6; :: thesis: verum

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