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;
A2: [#] (X | B) = B by PRE_TOPC:def 10;
A3: 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 A2;
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(A3);
then consider g being Function of the carrier of (X | B),the carrier of X such that
A4: for x being Element of (X | B) holds S₁[x,g . x] ;
A5: for p being Point of (X | B) holds g . p = p by A4;
A6: 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 A7: ( g . r0 in V & 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 A4;
then A9: r0 in W2 by A7, XBOOLE_0:def 4;
A10: 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
A11: ( x in dom g & x in W2 & y = g . x ) by FUNCT_1:def 12;
reconsider px = x as Point of (X | B) by A11;
g . px = px by A4;
hence y in V by A11, 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 A9, A10; :: thesis: verum

end;

reconsider g1 = g as Function of (X | B),X ;
g1 is continuous by A6, 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 A5; :: thesis: verum