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
the carrier of Sierpinski_Space = {0 ,1} by WAYBEL18:def 9;
then reconsider c = chi V,the carrier of T as Function of T,Sierpinski_Space ;
A1: [#] Sierpinski_Space <> {} ;
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: c " {0 ,1} = [#] T by FUNCT_2:48;

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, A4, ENUMSET1:def 1; :: thesis: verum

end;

hence chi V,the carrier of T is continuous Function of T,Sierpinski_Space by A1, TOPS_2:55; :: thesis: verum