let X, Y be non empty TopSpace; :: thesis: for f being Function of X,Y holds
( f is continuous iff for p being Point of X
for V being Subset of Y st f . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & f .: W c= V ) )
let f be Function of X,Y; :: thesis: ( f is continuous iff for p being Point of X
for V being Subset of Y st f . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & f .: W c= V ) )
A1: [#] Y <> {} ;
A2: dom f = the carrier of X by FUNCT_2:def 1;

hereby :: thesis: ( ( for p being Point of X
for V being Subset of Y st f . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & f .: W c= V ) ) implies f is continuous )

assume A3: f is continuous ; :: thesis: for p being Point of X
for V being Subset of Y st f . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & f .: W c= V )
thus for p being Point of X
for V being Subset of Y st f . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & f .: W c= V ) :: thesis: verum

proof

let p be Point of X; :: thesis: for V being Subset of Y st f . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & f .: W c= V )
let V be Subset of Y; :: thesis: ( f . p in V & V is open implies ex W being Subset of X st
( p in W & W is open & f .: W c= V ) )
assume ( f . p in V & V is open ) ; :: thesis: ex W being Subset of X st
( p in W & W is open & f .: W c= V )
then A4: ( f " V is open & p in f " V ) by A2, A1, A3, FUNCT_1:def 7, TOPS_2:43;
f .: (f " V) c= V by FUNCT_1:75;
hence ex W being Subset of X st
( p in W & W is open & f .: W c= V ) by A4; :: thesis: verum

end;

end;

assume A5: for p being Point of X
for V being Subset of Y st f . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & f .: W c= V ) ; :: thesis: f is continuous
for G being Subset of Y st G is open holds
f " G is open

proof

let G be Subset of Y; :: thesis: ( G is open implies f " G is open )
assume A6: G is open ; :: thesis: f " G is open
for z being set holds
( z in f " G iff ex Q being Subset of X st
( Q is open & Q c= f " G & z in Q ) )

proof

let z be set ; :: thesis: ( z in f " G iff ex Q being Subset of X st
( Q is open & Q c= f " G & z in Q ) )

now :: thesis: ( z in f " G implies ex Q being Subset of X st
( Q is open & Q c= f " G & z in Q ) )

assume A7: z in f " G ; :: thesis: ex Q being Subset of X st
( Q is open & Q c= f " G & z in Q )
then reconsider p = z as Point of X ;
f . z in G by A7, FUNCT_1:def 7;
then consider W being Subset of X such that
A8: ( p in W & W is open ) and
A9: f .: W c= G by A5, A6;
A10: W c= f " (f .: W) by A2, FUNCT_1:76;
f " (f .: W) c= f " G by A9, RELAT_1:143;
hence ex Q being Subset of X st
( Q is open & Q c= f " G & z in Q ) by A8, A10, XBOOLE_1:1; :: thesis: verum

end;

hence ( z in f " G iff ex Q being Subset of X st
( Q is open & Q c= f " G & z in Q ) ) ; :: thesis: verum

end;

hence f " G is open by TOPS_1:25; :: thesis: verum

end;

hence f is continuous by A1, TOPS_2:43; :: thesis: verum