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 Th45;
A3: c . x = 1 by A1, FUNCT_3:def 3;
A4: the carrier of Sierpinski_Space = {0,{0}} by WAYBEL18:def 9, CARD_1:49;
then reconsider i = (0,{0}) --> (y,x) as Function of Sierpinski_Space,T ;
A5: i . 1 = x by FUNCT_4:63, CARD_1:49;
A6: c . y = 0 by A2, FUNCT_3:def 3;
A7: i . 0 = y by FUNCT_4:63;
now :: thesis: ( c * i is Function of Sierpinski_Space,Sierpinski_Space & ( for a being Element of Sierpinski_Space holds (c * i) . a = (id Sierpinski_Space) . a ) )
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, CARD_1:49;
hence (c * i) . a = a by A7, A5, A3, A6, FUNCT_2:15
.= (id Sierpinski_Space) . a ;
:: thesis: verum
end;
hence (chi (V, the carrier of T)) * ((0,1) --> (y,x)) = id Sierpinski_Space by FUNCT_2:63, CARD_1:49; :: thesis: verum