let T be non empty TopSpace; :: thesis: for f being Function of R^1,T holds

( f is continuous iff for p being Point of R^1

for V being open Subset of T st f . p in V holds

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

let f be Function of R^1,T; :: thesis: ( f is continuous iff for p being Point of R^1

for V being open Subset of T st f . p in V holds

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

for V being open Subset of T st f . p in V holds

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

for p being Point of R^1

for V being Subset of T st f . p in V & V is open holds

ex W being Subset of R^1 st

( p in W & W is open & f .: W c= V )

( f is continuous iff for p being Point of R^1

for V being open Subset of T st f . p in V holds

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

let f be Function of R^1,T; :: thesis: ( f is continuous iff for p being Point of R^1

for V being open Subset of T st f . p in V holds

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

hereby :: thesis: ( ( for p being Point of R^1

for V being open Subset of T st f . p in V holds

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

assume A7:
for p being Point of R^1for V being open Subset of T st f . p in V holds

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

assume A1:
f is continuous
; :: thesis: for p being Point of R^1

for V being open Subset of T st f . p in V holds

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

let p be Point of R^1; :: thesis: for V being open Subset of T st f . p in V holds

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

let V be open Subset of T; :: thesis: ( f . p in V implies ex s being positive Real st f .: ].(p - s),(p + s).[ c= V )

assume f . p in V ; :: thesis: ex s being positive Real st f .: ].(p - s),(p + s).[ c= V

then consider W being Subset of R^1 such that

A2: p in W and

A3: W is open and

A4: f .: W c= V by A1, JGRAPH_2:10;

consider s being Real such that

A5: s > 0 and

A6: ].(p - s),(p + s).[ c= W by A2, A3, FRECHET:8;

reconsider s = s as positive Real by A5;

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

f .: ].(p - s),(p + s).[ c= f .: W by A6, RELAT_1:123;

hence f .: ].(p - s),(p + s).[ c= V by A4; :: thesis: verum

end;for V being open Subset of T st f . p in V holds

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

let p be Point of R^1; :: thesis: for V being open Subset of T st f . p in V holds

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

let V be open Subset of T; :: thesis: ( f . p in V implies ex s being positive Real st f .: ].(p - s),(p + s).[ c= V )

assume f . p in V ; :: thesis: ex s being positive Real st f .: ].(p - s),(p + s).[ c= V

then consider W being Subset of R^1 such that

A2: p in W and

A3: W is open and

A4: f .: W c= V by A1, JGRAPH_2:10;

consider s being Real such that

A5: s > 0 and

A6: ].(p - s),(p + s).[ c= W by A2, A3, FRECHET:8;

reconsider s = s as positive Real by A5;

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

f .: ].(p - s),(p + s).[ c= f .: W by A6, RELAT_1:123;

hence f .: ].(p - s),(p + s).[ c= V by A4; :: thesis: verum

for V being open Subset of T st f . p in V holds

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

for p being Point of R^1

for V being Subset of T st f . p in V & V is open holds

ex W being Subset of R^1 st

( p in W & W is open & f .: W c= V )

proof

hence
f is continuous
by JGRAPH_2:10; :: thesis: verum
let p be Point of R^1; :: thesis: for V being Subset of T st f . p in V & V is open holds

ex W being Subset of R^1 st

( p in W & W is open & f .: W c= V )

let V be Subset of T; :: thesis: ( f . p in V & V is open implies ex W being Subset of R^1 st

( p in W & W is open & f .: W c= V ) )

assume that

A8: f . p in V and

A9: V is open ; :: thesis: ex W being Subset of R^1 st

( p in W & W is open & f .: W c= V )

consider s being positive Real such that

A10: f .: ].(p - s),(p + s).[ c= V by A7, A8, A9;

take W = R^1 ].(p - s),(p + s).[; :: thesis: ( p in W & W is open & f .: W c= V )

thus p in W by TOPREAL6:15; :: thesis: ( W is open & f .: W c= V )

thus W is open ; :: thesis: f .: W c= V

thus f .: W c= V by A10; :: thesis: verum

end;ex W being Subset of R^1 st

( p in W & W is open & f .: W c= V )

let V be Subset of T; :: thesis: ( f . p in V & V is open implies ex W being Subset of R^1 st

( p in W & W is open & f .: W c= V ) )

assume that

A8: f . p in V and

A9: V is open ; :: thesis: ex W being Subset of R^1 st

( p in W & W is open & f .: W c= V )

consider s being positive Real such that

A10: f .: ].(p - s),(p + s).[ c= V by A7, A8, A9;

take W = R^1 ].(p - s),(p + s).[; :: thesis: ( p in W & W is open & f .: W c= V )

thus p in W by TOPREAL6:15; :: thesis: ( W is open & f .: W c= V )

thus W is open ; :: thesis: f .: W c= V

thus f .: W c= V by A10; :: thesis: verum