let T be non empty TopSpace; :: thesis: for V being open Subset of T holds chi V,the carrier of T is continuous Function of T,Sierpinski_Space
let V be open Subset of T; :: thesis: chi V,the carrier of T is continuous Function of T,Sierpinski_Space
reconsider c = chi V,the carrier of T as Function of T,Sierpinski_Space by WAYBEL18:def 9;
A1: c " {0 ,1} = [#] T by FUNCT_2:48;
c = chi (c " {1}),the carrier of T by FUNCT_3:49;
then A2: V = c " {1} by FUNCT_3:47;
A3: c " {} = {} T by RELAT_1:171;

A4: now

let W be Subset of Sierpinski_Space ; :: thesis: ( W is open implies c " W is open )
assume W is open ; :: thesis: c " W is open
then W in the topology of Sierpinski_Space by PRE_TOPC:def 5;
then W in {{} ,{1},{0 ,1}} by WAYBEL18:def 9;
hence c " W is open by A2, A3, A1, ENUMSET1:def 1; :: thesis: verum

end;

[#] Sierpinski_Space <> {} ;
hence chi V,the carrier of T is continuous Function of T,Sierpinski_Space by A4, TOPS_2:55; :: thesis: verum