reconsider 00 = 0 , 01 = 1 as Element of I[01] by BORSUK_1:40, XXREAL_1:1;
let x be Real; for w being Rational ex f being continuous Function of Sorgenfrey-line,I[01] st
for a being Point of Sorgenfrey-line holds
( ( a in [.x,w.[ implies f . a = 0 ) & ( not a in [.x,w.[ implies f . a = 1 ) )
set X = Sorgenfrey-line ;
let w be Rational; ex f being continuous Function of Sorgenfrey-line,I[01] st
for a being Point of Sorgenfrey-line holds
( ( a in [.x,w.[ implies f . a = 0 ) & ( not a in [.x,w.[ implies f . a = 1 ) )
reconsider V = [.x,w.[ as open closed Subset of Sorgenfrey-line by Th57, TOPGEN_3:11;
defpred S1[ object ] means $1 in [.x,w.[;
deffunc H1( object ) -> Element of omega = 0 ;
deffunc H2( object ) -> Element of omega = 1;
reconsider f1 = (Sorgenfrey-line | V) --> 00 as continuous Function of (Sorgenfrey-line | V),I[01] ;
reconsider f2 = (Sorgenfrey-line | (V `)) --> 01 as continuous Function of (Sorgenfrey-line | (V `)),I[01] ;
A1:
for a being object st a in the carrier of Sorgenfrey-line holds
( ( S1[a] implies H1(a) in the carrier of I[01] ) & ( not S1[a] implies H2(a) in the carrier of I[01] ) )
by BORSUK_1:40, XXREAL_1:1;
consider f being Function of Sorgenfrey-line,I[01] such that
A2:
for a being object st a in the carrier of Sorgenfrey-line holds
( ( S1[a] implies f . a = H1(a) ) & ( not S1[a] implies f . a = H2(a) ) )
from FUNCT_2:sch 5(A1);
the carrier of (Sorgenfrey-line | V) = V
by PRE_TOPC:8;
then A4:
dom f1 = V
;
A5:
the carrier of (Sorgenfrey-line | (V `)) = V `
by PRE_TOPC:8;
then A6:
dom f2 = V `
;
A7:
dom f = [#] Sorgenfrey-line
by FUNCT_2:def 1;
V \/ (V `) = [#] Sorgenfrey-line
by PRE_TOPC:2;
then
f = f1 +* f2
by A8, A7, A4, A6, FUNCT_4:def 1;
then reconsider f = f as continuous Function of Sorgenfrey-line,I[01] by Th12;
take
f
; for a being Point of Sorgenfrey-line holds
( ( a in [.x,w.[ implies f . a = 0 ) & ( not a in [.x,w.[ implies f . a = 1 ) )
let a be Point of Sorgenfrey-line; ( ( a in [.x,w.[ implies f . a = 0 ) & ( not a in [.x,w.[ implies f . a = 1 ) )
thus
( ( a in [.x,w.[ implies f . a = 0 ) & ( not a in [.x,w.[ implies f . a = 1 ) )
by A2; verum