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 that
A1: x in V and
A2: not y in V ; :: thesis: (chi V,the carrier of T) * (0 ,1 --> y,x) = id Sierpinski_Space
reconsider c = chi V,the carrier of T as Function of T,Sierpinski_Space by Th48;
A3: c . x = 1 by A1, FUNCT_3:def 3;
A4: the carrier of Sierpinski_Space = {0 ,1} by WAYBEL18:def 9;
then reconsider i = 0 ,1 --> y,x as Function of Sierpinski_Space ,T ;
A5: i . 1 = x by FUNCT_4:66;
A6: c . y = 0 by A2, FUNCT_3:def 3;
A7: i . 0 = y by FUNCT_4:66;

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 A4, TARSKI:def 2;
hence (c * i) . a = a by A7, A5, A3, A6, 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