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_{1}[ 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 S_{1}[x,y]

for x being Element of (X | B) holds S_{1}[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_{1}[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 )

g1 is continuous by A5, JGRAPH_2:10;

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

( ( 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

A1: [#] (X | B) = B by PRE_TOPC:def 5;

A2: for x being Element of (X | B) ex y being Element of X st S

proof

ex g being Function of the carrier of (X | B), the carrier of X st
let x be Element of (X | B); :: thesis: ex y being Element of X st S_{1}[x,y]

x in B by A1;

then reconsider px = x as Point of X ;

set y0 = px;

S_{1}[x,px]
;

hence ex y being Element of X st S_{1}[x,y]
; :: thesis: verum

end;x in B by A1;

then reconsider px = x as Point of X ;

set y0 = px;

S

hence ex y being Element of X st S

for x being Element of (X | B) holds S

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

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

reconsider g1 = g as Function of (X | B),X ;
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:24;

g .: W2 c= V

( r0 in W & W is open & g .: W c= V ) by A8, A9; :: thesis: verum

end;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:24;

g .: W2 c= V

proof

hence
ex W being Subset of (X | B) st
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 A11, A12, XBOOLE_0:def 4; :: thesis: verum

end;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 A11, A12, XBOOLE_0:def 4; :: thesis: verum

( r0 in W & W is open & g .: W c= V ) by A8, A9; :: thesis: verum

g1 is continuous by A5, JGRAPH_2:10;

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