reconsider 00 = 0 , 01 = 1 as Element of I[01] by BORSUK_1:40, XXREAL_1:1;
let x be real number ; :: thesis: for w being rational number 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 number ; :: 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 Th61, TOPGEN_3:11;
defpred S₁[ set ] means $1 in [.x,w.[;
deffunc H₁( set ) -> Element of NAT = 0 ;
deffunc H₂( set ) -> Element of NAT = 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 set st a in the carrier of Sorgenfrey-line holds
( ( S₁[a] implies H₁(a) in the carrier of I[01] ) & ( not S₁[a] implies H₂(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 set st a in the carrier of Sorgenfrey-line holds
( ( S₁[a] implies f . a = H₁(a) ) & ( not S₁[a] implies f . a = H₂(a) ) ) from FUNCT_2:sch 5(A1);
A3: the carrier of (Sorgenfrey-line | V) = V by PRE_TOPC:8;
then A4: dom f1 = V by FUNCT_2:def 1;
A5: the carrier of (Sorgenfrey-line | (V `)) = V ` by PRE_TOPC:8;
then A6: dom f2 = V ` by FUNCT_2:def 1;
A7: dom f = [#] Sorgenfrey-line by FUNCT_2:def 1;

A8: now

let u be set ; :: 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 A11: x in V by A6, SUBSET_1:29;
hence f . u = 0 by A2
.= f1 . u by A3, A11, FUNCOP_1:7 ;
:: 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 Th16;
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