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 S1[ set , set ] means for p being Point of (X | B) holds \$2 = \$1;
A1: [#] (X | B) = B by PRE_TOPC:def 5;
A2: for x being Element of (X | B) ex y being Element of X st S1[x,y]
proof
let x be Element of (X | B); :: thesis: ex y being Element of X st S1[x,y]
x in B by A1;
then reconsider px = x as Point of X ;
set y0 = px;
S1[x,px] ;
hence
ex y being Element of X st S1[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 S1[x,g . x] from 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 S1[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 ;
A9: W2 is open by ;
g .: W2 c= V
proof
let y be object ; :: 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 object such that
A10: x in dom g and
A11: x in W2 and
A12: y = g . x by FUNCT_1:def 6;
reconsider px = x as Point of (X | B) by A10;
g . px = px by A3;
hence y in V by ; :: 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 ;
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