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

proof

let x be Element of (X | B); :: thesis: ex y being Element of X st S₁[x,y]
x in B by A1;
then reconsider px = x as Point of X ;
set y0 = px;
S₁[x,px] ;
hence ex y being Element of X 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 (X | B) 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 (X | B) holds S₁[x,g . x] ;
A4: for p being Point of (X | B) holds g . p = p by A3;
A5: for r0 being Point of (X | B)
for V being Subset of X st g . r0 in V & V is open holds
ex W being Subset of (X | B) st
( r0 in W & W is open & g .: W c= V )

proof

let r0 be Point of (X | B); :: thesis: for V being Subset of X st g . r0 in V & V is open holds
ex W being Subset of (X | B) st
( r0 in W & W is open & g .: W c= V )
let V be Subset of X; :: thesis: ( g . r0 in V & V is open implies ex W being Subset of (X | B) 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 (X | B) st
( r0 in W & W is open & g .: W c= V )
reconsider W2 = V /\ ([#] (X | B)) as Subset of (X | B) ;
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 (X | B) 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 (X | B) 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 (X | B) holds f . p = p ) & f is continuous ) by A4; :: thesis: verum