let X, Y be non empty TopSpace; :: thesis: for f being Function of X,Y

for x being Point of X holds

( f is_continuous_at x iff for G being a_neighborhood of f . x holds f " G is a_neighborhood of x )

let f be Function of X,Y; :: thesis: for x being Point of X holds

( f is_continuous_at x iff for G being a_neighborhood of f . x holds f " G is a_neighborhood of x )

let x be Point of X; :: thesis: ( f is_continuous_at x iff for G being a_neighborhood of f . x holds f " G is a_neighborhood of x )

thus ( f is_continuous_at x implies for G being a_neighborhood of f . x holds f " G is a_neighborhood of x ) :: thesis: ( ( for G being a_neighborhood of f . x holds f " G is a_neighborhood of x ) implies f is_continuous_at x )

let G be a_neighborhood of f . x; :: according to TMAP_1:def 2 :: thesis: ex H being a_neighborhood of x st f .: H c= G

reconsider H = f " G as a_neighborhood of x by A4;

take H ; :: thesis: f .: H c= G

thus f .: H c= G by FUNCT_1:75; :: thesis: verum

for x being Point of X holds

( f is_continuous_at x iff for G being a_neighborhood of f . x holds f " G is a_neighborhood of x )

let f be Function of X,Y; :: thesis: for x being Point of X holds

( f is_continuous_at x iff for G being a_neighborhood of f . x holds f " G is a_neighborhood of x )

let x be Point of X; :: thesis: ( f is_continuous_at x iff for G being a_neighborhood of f . x holds f " G is a_neighborhood of x )

thus ( f is_continuous_at x implies for G being a_neighborhood of f . x holds f " G is a_neighborhood of x ) :: thesis: ( ( for G being a_neighborhood of f . x holds f " G is a_neighborhood of x ) implies f is_continuous_at x )

proof

assume A4:
for G being a_neighborhood of f . x holds f " G is a_neighborhood of x
; :: thesis: f is_continuous_at x
assume A1:
f is_continuous_at x
; :: thesis: for G being a_neighborhood of f . x holds f " G is a_neighborhood of x

let G be a_neighborhood of f . x; :: thesis: f " G is a_neighborhood of x

consider H being a_neighborhood of x such that

A2: f .: H c= G by A1;

ex V being Subset of X st

( V is open & V c= f " G & x in V )

end;let G be a_neighborhood of f . x; :: thesis: f " G is a_neighborhood of x

consider H being a_neighborhood of x such that

A2: f .: H c= G by A1;

ex V being Subset of X st

( V is open & V c= f " G & x in V )

proof

hence
f " G is a_neighborhood of x
by CONNSP_2:6; :: thesis: verum
consider V being Subset of X such that

A3: ( V is open & V c= H & x in V ) by CONNSP_2:6;

take V ; :: thesis: ( V is open & V c= f " G & x in V )

H c= f " G by A2, FUNCT_2:95;

hence ( V is open & V c= f " G & x in V ) by A3, XBOOLE_1:1; :: thesis: verum

end;A3: ( V is open & V c= H & x in V ) by CONNSP_2:6;

take V ; :: thesis: ( V is open & V c= f " G & x in V )

H c= f " G by A2, FUNCT_2:95;

hence ( V is open & V c= f " G & x in V ) by A3, XBOOLE_1:1; :: thesis: verum

let G be a_neighborhood of f . x; :: according to TMAP_1:def 2 :: thesis: ex H being a_neighborhood of x st f .: H c= G

reconsider H = f " G as a_neighborhood of x by A4;

take H ; :: thesis: f .: H c= G

thus f .: H c= G by FUNCT_1:75; :: thesis: verum