let T be non empty TopSpace; :: thesis: for x, y being Element of T
for V being open Subset of T st x in V & not y in V holds
(chi V,the carrier of T) * (0 ,1 --> y,x) = id Sierpinski_Space
let x, y be Element of T; :: thesis: for V being open Subset of T st x in V & not y in V holds
(chi V,the carrier of T) * (0 ,1 --> y,x) = id Sierpinski_Space
let V be open Subset of T; :: thesis: ( x in V & not y in V implies (chi V,the carrier of T) * (0 ,1 --> y,x) = id Sierpinski_Space )
assume A1: ( x in V & not y in V ) ; :: thesis: (chi V,the carrier of T) * (0 ,1 --> y,x) = id Sierpinski_Space
A2: the carrier of Sierpinski_Space = {0 ,1} by WAYBEL18:def 9;
then reconsider i = 0 ,1 --> y,x as Function of Sierpinski_Space ,T ;
reconsider c = chi V,the carrier of T as Function of T,Sierpinski_Space by Th48;
A3: ( i . 0 = y & i . 1 = x ) by FUNCT_4:66;
A4: ( c . x = 1 & c . y = 0 ) by A1, FUNCT_3:def 3;

now

thus c * i is Function of Sierpinski_Space ,Sierpinski_Space ; :: thesis: for a being Element of Sierpinski_Space holds (c * i) . a = (id Sierpinski_Space ) . a
let a be Element of Sierpinski_Space ; :: thesis: (c * i) . a = (id Sierpinski_Space ) . a
( a = 0 or a = 1 ) by A2, TARSKI:def 2;
hence (c * i) . a = a by A3, A4, FUNCT_2:21
.= (id Sierpinski_Space ) . a by FUNCT_1:35 ;
:: thesis: verum

end;

hence (chi V,the carrier of T) * (0 ,1 --> y,x) = id Sierpinski_Space by FUNCT_2:113; :: thesis: verum