let X be non empty TopSpace; :: thesis: for B being non empty Subset of ex f being Function of (X | B),X st
( ( for p being Point of holds f . p = p ) & f is continuous )
let B be non empty Subset of ; :: thesis: ex f being Function of (X | B),X st
( ( for p being Point of holds f . p = p ) & f is continuous )
defpred S₁[ set , set ] means for p being Point of holds $2 = $1;
A1: [#] (X | B) = B by PRE_TOPC:def 10;
A2: for x being Element of ex y being Element of st S₁[x,y]

proof

let x be Element of ; :: thesis: ex y being Element of st S₁[x,y]
x in B by A1;
then reconsider px = x as Point of ;
set y0 = px;
S₁[x,px] ;
hence ex y being Element of st S₁[x,y] ; :: thesis: verum

end;

ex g being Function of the carrier of (X | B),the carrier of X st
for x being Element of holds S₁[x,g . x] from FUNCT_2:sch 3(A2);
then consider g being Function of the carrier of (X | B),the carrier of X such that
A3: for x being Element of holds S₁[x,g . x] ;
A4: for p being Point of holds g . p = p by A3;
A5: for r0 being Point of
for V being Subset of st g . r0 in V & V is open holds
ex W being Subset of st
( r0 in W & W is open & g .: W c= V )

proof

let r0 be Point of ; :: thesis: for V being Subset of st g . r0 in V & V is open holds
ex W being Subset of st
( r0 in W & W is open & g .: W c= V )
let V be Subset of ; :: thesis: ( g . r0 in V & V is open implies ex W being Subset of st
( r0 in W & W is open & g .: W c= V ) )
assume that
A6: g . r0 in V and
A7: V is open ; :: thesis: ex W being Subset of st
( r0 in W & W is open & g .: W c= V )
reconsider W2 = V /\ ([#] (X | B)) as Subset of ;
g . r0 = r0 by A3;
then A8: r0 in W2 by A6, XBOOLE_0:def 4;
A9: W2 is open by A7, TOPS_2:32;
g .: W2 c= V

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in g .: W2 or y in V )
assume y in g .: W2 ; :: thesis: y in V
then consider x being set such that
A10: x in dom g and
A11: x in W2 and
A12: y = g . x by FUNCT_1:def 12;
reconsider px = x as Point of by A10;
g . px = px by A3;
hence y in V by A11, A12, XBOOLE_0:def 4; :: thesis: verum

end;

hence ex W being Subset of st
( r0 in W & W is open & g .: W c= V ) by A8, A9; :: thesis: verum

end;

reconsider g1 = g as Function of (X | B),X ;
g1 is continuous by A5, JGRAPH_2:20;
hence ex f being Function of (X | B),X st
( ( for p being Point of holds f . p = p ) & f is continuous ) by A4; :: thesis: verum