reconsider 00 = 0 , 01 = 1 as Element of I[01] by BORSUK_1:40, XXREAL_1:1;
let x be Real; :: thesis: 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; :: thesis: 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;
A8: now :: thesis: for u being object st u in (dom f1) \/ (dom f2) holds
( ( u in dom f2 implies f . u = f2 . u ) & ( not u in dom f2 implies f . u = f1 . u ) )
let u be object ; :: thesis: ( u in (dom f1) \/ (dom f2) implies ( ( u in dom f2 implies f . u = f2 . u ) & ( not u in dom f2 implies f . u = f1 . u ) ) )
assume u in (dom f1) \/ (dom f2) ; :: thesis: ( ( u in dom f2 implies f . u = f2 . u ) & ( not u in dom f2 implies f . u = f1 . u ) )
then reconsider x = u as Point of Sorgenfrey-line by A7, A4, A6, PRE_TOPC:2;
hereby :: thesis: ( not u in dom f2 implies f . u = f1 . u )
assume A9: u in dom f2 ; :: thesis: f . u = f2 . u
then A10: ((V `) --> 1) . u = 1 by A5, FUNCOP_1:7;
not x in V by A9, A5, XBOOLE_0:def 5;
hence f . u = f2 . u by A10, A5, A2; :: thesis: verum
end;
assume not u in dom f2 ; :: thesis: f . u = f1 . u
then x in V by A6, SUBSET_1:29;
hence f . u = 0 by A2
.= f1 . u ;
:: thesis: verum
end;
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 ; :: thesis: 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; :: thesis: ( ( 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; :: thesis: verum