A1: [#] Y <> {} ;
thus ( F is continuous implies for W being Point of X
for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G ) :: thesis: ( ( for W being Point of X
for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G ) implies F is continuous )

proof

assume A2: F is continuous ; :: thesis: for W being Point of X
for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G
let W be Point of X; :: thesis: for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G
let G be a_neighborhood of F . W; :: thesis: ex H being a_neighborhood of W st F .: H c= G
F . W in Int G by CONNSP_2:def 1;
then A3: W in F " (Int G) by FUNCT_2:38;
F " (Int G) is open by A1, A2, TOPS_2:43;
then W in Int (F " (Int G)) by A3, TOPS_1:23;
then reconsider H = F " (Int G) as a_neighborhood of W by CONNSP_2:def 1;
take H ; :: thesis: F .: H c= G
H c= F " G by RELAT_1:143, TOPS_1:16;
hence F .: H c= G by EQREL_1:46; :: thesis: verum

end;

assume A4: for W being Point of X
for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G ; :: thesis: F is continuous

now

let P1 be Subset of Y; :: thesis: ( P1 is open implies F " P1 is open )
assume A5: P1 is open ; :: thesis: F " P1 is open

now

let x be set ; :: thesis: ( ( x in F " P1 implies ex P being Subset of X st
( P is open & P c= F " P1 & x in P ) ) & ( ex P being Subset of X st
( P is open & P c= F " P1 & x in P ) implies x in F " P1 ) )
thus ( x in F " P1 implies ex P being Subset of X st
( P is open & P c= F " P1 & x in P ) ) :: thesis: ( ex P being Subset of X st
( P is open & P c= F " P1 & x in P ) implies x in F " P1 )

proof

assume A6: x in F " P1 ; :: thesis: ex P being Subset of X st
( P is open & P c= F " P1 & x in P )
then reconsider W = x as Point of X ;
A7: Int P1 = P1 by A5, TOPS_1:23;
F . W in P1 by A6, FUNCT_2:38;
then P1 is a_neighborhood of F . W by A7, CONNSP_2:def 1;
then consider H being a_neighborhood of W such that
A8: F .: H c= P1 by A4;
take Int H ; :: thesis: ( Int H is open & Int H c= F " P1 & x in Int H )
thus Int H is open ; :: thesis: ( Int H c= F " P1 & x in Int H )
A9: Int H c= H by TOPS_1:16;
dom F = the carrier of X by FUNCT_2:def 1;
then A10: H c= F " (F .: H) by FUNCT_1:76;
F " (F .: H) c= F " P1 by A8, RELAT_1:143;
then H c= F " P1 by A10, XBOOLE_1:1;
hence Int H c= F " P1 by A9, XBOOLE_1:1; :: thesis: x in Int H
thus x in Int H by CONNSP_2:def 1; :: thesis: verum

end;

thus ( ex P being Subset of X st
( P is open & P c= F " P1 & x in P ) implies x in F " P1 ) ; :: thesis: verum

end;

hence F " P1 is open by TOPS_1:25; :: thesis: verum

end;

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