let S be non empty TopSpace; :: thesis: for T being NormedLinearTopSpace
for f being Function of S,T
for x being Point of S holds
( f is_continuous_at x iff for e being Real st 0 < e holds
ex H being Subset of S st
( H is open & x in H & ( for y being Point of S st y in H holds
||.((f . x) - (f . y)).|| < e ) ) )
let T be NormedLinearTopSpace; :: thesis: for f being Function of S,T
for x being Point of S holds
( f is_continuous_at x iff for e being Real st 0 < e holds
ex H being Subset of S st
( H is open & x in H & ( for y being Point of S st y in H holds
||.((f . x) - (f . y)).|| < e ) ) )
let f be Function of S,T; :: thesis: for x being Point of S holds
( f is_continuous_at x iff for e being Real st 0 < e holds
ex H being Subset of S st
( H is open & x in H & ( for y being Point of S st y in H holds
||.((f . x) - (f . y)).|| < e ) ) )
let x be Point of S; :: thesis: ( f is_continuous_at x iff for e being Real st 0 < e holds
ex H being Subset of S st
( H is open & x in H & ( for y being Point of S st y in H holds
||.((f . x) - (f . y)).|| < e ) ) )

hereby :: thesis: ( ( for e being Real st 0 < e holds
ex H being Subset of S st
( H is open & x in H & ( for y being Point of S st y in H holds
||.((f . x) - (f . y)).|| < e ) ) ) implies f is_continuous_at x )

assume A1: f is_continuous_at x ; :: thesis: for e being Real st 0 < e holds
ex H being Subset of S st
( H is open & x in H & ( for y being Point of S st y in H holds
||.((f . x) - (f . y)).|| < e ) )
let e be Real; :: thesis: ( 0 < e implies ex H being Subset of S st
( H is open & x in H & ( for y being Point of S st y in H holds
||.((f . x) - (f . y)).|| < e ) ) )
assume A2: 0 < e ; :: thesis: ex H being Subset of S st
( H is open & x in H & ( for y being Point of S st y in H holds
||.((f . x) - (f . y)).|| < e ) )
set V = { y where y is Point of T : ||.((f . x) - y).|| < e } ;

now :: thesis: for z being object st z in { y where y is Point of T : ||.((f . x) - y).|| < e } holds
z in the carrier of T

let z be object ; :: thesis: ( z in { y where y is Point of T : ||.((f . x) - y).|| < e } implies z in the carrier of T )
assume z in { y where y is Point of T : ||.((f . x) - y).|| < e } ; :: thesis: z in the carrier of T
then ex y being Point of T st
( z = y & ||.((f . x) - y).|| < e ) ;
hence z in the carrier of T ; :: thesis: verum

end;

then reconsider V = { y where y is Point of T : ||.((f . x) - y).|| < e } as Subset of T by TARSKI:def 3;
||.((f . x) - (f . x)).|| < e by NORMSP_1:6, A2;
then f . x in V ;
then consider H being Subset of S such that
A3: ( H is open & x in H & f .: H c= V ) by A1, TMAP_1:43, C0SP3:24;
take H = H; :: thesis: ( H is open & x in H & ( for y being Point of S st y in H holds
||.((f . x) - (f . y)).|| < e ) )
thus H is open by A3; :: thesis: ( x in H & ( for y being Point of S st y in H holds
||.((f . x) - (f . y)).|| < e ) )
thus x in H by A3; :: thesis: for y being Point of S st y in H holds
||.((f . x) - (f . y)).|| < e
let y be Point of S; :: thesis: ( y in H implies ||.((f . x) - (f . y)).|| < e )
assume y in H ; :: thesis: ||.((f . x) - (f . y)).|| < e
then f . y in f .: H by FUNCT_2:35;
then f . y in V by A3;
then ex z being Point of T st
( z = f . y & ||.((f . x) - z).|| < e ) ;
hence ||.((f . x) - (f . y)).|| < e ; :: thesis: verum

end;

assume A4: for e being Real st 0 < e holds
ex H being Subset of S st
( H is open & x in H & ( for y being Point of S st y in H holds
||.((f . x) - (f . y)).|| < e ) ) ; :: thesis: f is_continuous_at x
for G being Subset of T st G is open & f . x in G holds
ex H being Subset of S st
( H is open & x in H & f .: H c= G )

proof

let G be Subset of T; :: thesis: ( G is open & f . x in G implies ex H being Subset of S st
( H is open & x in H & f .: H c= G ) )
assume ( G is open & f . x in G ) ; :: thesis: ex H being Subset of S st
( H is open & x in H & f .: H c= G )
then consider r being Real such that
A5: ( r > 0 & { y where y is Point of T : ||.((f . x) - y).|| < r } c= G ) by C0SP3:23;
consider H being Subset of S such that
A6: ( H is open & x in H & ( for y being Point of S st y in H holds
||.((f . x) - (f . y)).|| < r ) ) by A4, A5;
take H ; :: thesis: ( H is open & x in H & f .: H c= G )
thus H is open by A6; :: thesis: ( x in H & f .: H c= G )
thus x in H by A6; :: thesis: f .: H c= G

now :: thesis: for z being object st z in f .: H holds
z in G

let z be object ; :: thesis: ( z in f .: H implies z in G )
assume z in f .: H ; :: thesis: z in G
then consider t being object such that
A7: ( t in dom f & t in H & z = f . t ) by FUNCT_1:def 6;
reconsider t = t as Point of S by A7;
||.((f . x) - (f . t)).|| < r by A7, A6;
then z in { y where y is Point of T : ||.((f . x) - y).|| < r } by A7;
hence z in G by A5; :: thesis: verum

end;

hence f .: H c= G ; :: thesis: verum

end;

hence f is_continuous_at x by TMAP_1:43; :: thesis: verum