let X be non empty TopSpace; :: according to WAYBEL18:def 5 :: thesis:
set S = Sierpinski_Space ;
let f be Function of X,Sierpinski_Space; :: thesis:
A1: [#] Sierpinski_Space <> {} ;
{1} c= {0,1} by ZFMISC_1:7;
then reconsider u = {1} as Subset of Sierpinski_Space by Def9;
u in {{},{1},{0,1}} by ENUMSET1:def 1;
then u in the topology of Sierpinski_Space by Def9;
then A2: u is open ;
assume f is continuous ; :: thesis:
then f " u is open by A1, A2, TOPS_2:43;
then A3: f " u in the topology of X ;
let Y be non empty TopSpace; :: thesis:
assume A4: X is SubSpace of Y ; :: thesis:
then consider V being Subset of Y such that
A5: V in the topology of Y and
A6: f " u = V /\ ([#] X) by A3, PRE_TOPC:def 4;
reconsider V = V as Subset of Y ;
set g = chi (V, the carrier of Y);
A7: dom (chi (V, the carrier of Y)) = the carrier of Y by FUNCT_3:def 3;
reconsider g = chi (V, the carrier of Y) as Function of Y,Sierpinski_Space by Def9;
A8: the carrier of X c= the carrier of Y by A4, BORSUK_1:1;
A9: for x being object st x in dom f holds
f . x = g . x

proof

let x be object ; :: thesis:
assume A10: x in dom f ; :: thesis:
then A11: x in the carrier of X ;

per cases ;

suppose A12: x in V ; :: thesis:

then x in f " u by A6, A10, XBOOLE_0:def 4;
then A13: f . x in {1} by FUNCT_1:def 7;
g . x = 1 by A12, FUNCT_3:def 3;
hence f . x = g . x by A13, TARSKI:def 1; :: thesis:

end;

suppose A14: not x in V ; :: thesis:

f . x in rng f by A10, FUNCT_1:def 3;
then f . x in the carrier of Sierpinski_Space ;
then f . x in {0,1} by Def9;
then A15: ( f . x = 0 or f . x = 1 ) by TARSKI:def 2;
not x in f " {1} by A6, A14, XBOOLE_0:def 4;
then ( not x in dom f or not f . x in {1} ) by FUNCT_1:def 7;
hence f . x = g . x by A8, A10, A11, A14, A15, FUNCT_3:def 3, TARSKI:def 1; :: thesis:

end;

end;

end;

take g ; :: thesis:
A16: V is open by A5;
for P being Subset of Sierpinski_Space st P is open holds
g " P is open

proof

let P be Subset of Sierpinski_Space; :: thesis:
assume P is open ; :: thesis:
then P in the topology of Sierpinski_Space ;
then A17: P in {{},{1},{0,1}} by Def9;

per cases by A17, ENUMSET1:def 1;

suppose P = {} ; :: thesis:

then g " P = {} ;
then g " P in the topology of Y by PRE_TOPC:1;
hence g " P is open ; :: thesis:

end;

suppose A18: P = {1} ; :: thesis:

A19: g " P c= V

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A20: x in g " P ; :: thesis:
then g . x in {1} by A18, FUNCT_1:def 7;
then g . x = 1 by TARSKI:def 1;
hence x in V by A20, FUNCT_3:def 3; :: thesis:

end;

V c= g " P

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A21: x in V ; :: thesis:
then g . x = 1 by FUNCT_3:def 3;
then g . x in {1} by TARSKI:def 1;
hence x in g " P by A7, A18, A21, FUNCT_1:def 7; :: thesis:

end;

hence g " P is open by A16, A19, XBOOLE_0:def 10; :: thesis:

end;

suppose P = {0,1} ; :: thesis:

then g " P = the carrier of Y by FUNCT_2:40;
then g " P in the topology of Y by PRE_TOPC:def 1;
hence g " P is open ; :: thesis:

end;

end;

end;

hence g is continuous by A1, TOPS_2:43; :: thesis:
(dom g) /\ the carrier of X = the carrier of Y /\ the carrier of X by FUNCT_3:def 3
.= the carrier of X by A4, BORSUK_1:1, XBOOLE_1:28
.= dom f by FUNCT_2:def 1 ;
hence g | the carrier of X = f by A9, FUNCT_1:46; :: thesis: