let T be non empty normal TopSpace; :: thesis:
let A, B be closed Subset of T; :: thesis:
assume A1: ( A <> {} & A misses B ) ; :: thesis:
let G be Rain of A,B; :: thesis:
defpred S₁[ Element of DOM , set ] means ( ( $1 in halfline 0 implies $2 = {} ) & ( $1 in right_open_halfline 1 implies $2 = the carrier of T ) & ( $1 in DYADIC implies for n being Nat st $1 in dyadic n holds
$2 = (G . n) . $1 ) );
A2: for x being Element of DOM ex y being Subset of T st S₁[x,y]

proof

reconsider a = 0 , b = 1 as R_eal by XXREAL_0:def 1;
let x be Element of DOM ; :: thesis:
A3: ( x in (halfline 0) \/ DYADIC or x in right_open_halfline 1 ) by URYSOHN1:def 3, XBOOLE_0:def 3;

per cases by A3, XBOOLE_0:def 3;

suppose A4: x in halfline 0 ; :: thesis:

A5: ( not x in right_open_halfline 1 & not x in DYADIC )

proof

assume A6: ( x in right_open_halfline 1 or x in DYADIC ) ; :: thesis:

per cases by A6;

suppose x in right_open_halfline 1 ; :: thesis:

then 1 < x by XXREAL_1:235;
hence contradiction by A4, XXREAL_1:233; :: thesis:

end;

suppose A7: x in DYADIC ; :: thesis:

reconsider x = x as R_eal by XXREAL_0:def 1;
a <= x by A7, URYSOHN2:28, XXREAL_1:1;
hence contradiction by A4, XXREAL_1:233; :: thesis:

end;

end;

end;

reconsider s = {} as Subset of T by XBOOLE_1:2;
s = s ;
hence ex y being Subset of T st S₁[x,y] by A5; :: thesis:

end;

suppose A8: x in DYADIC ; :: thesis:

A9: not x in halfline 0

proof

assume A10: x in halfline 0 ; :: thesis:
reconsider x = x as R_eal by XXREAL_0:def 1;
a <= x by A8, URYSOHN2:28, XXREAL_1:1;
hence contradiction by A10, XXREAL_1:233; :: thesis:

end;

A11: not x in right_open_halfline 1

proof

assume A12: x in right_open_halfline 1 ; :: thesis:
reconsider x = x as R_eal by XXREAL_0:def 1;
x <= b by A8, URYSOHN2:28, XXREAL_1:1;
hence contradiction by A12, XXREAL_1:235; :: thesis:

end;

ex s being Subset of T st
for n being Nat st x in dyadic n holds
s = (G . n) . x by A1, A8, Th9;
hence ex y being Subset of T st S₁[x,y] by A11, A9; :: thesis:

end;

suppose A13: x in right_open_halfline 1 ; :: thesis:

A14: ( not x in halfline 0 & not x in DYADIC )

proof

assume A15: ( x in halfline 0 or x in DYADIC ) ; :: thesis:

per cases by A15;

suppose x in halfline 0 ; :: thesis:

then x < 0 by XXREAL_1:233;
hence contradiction by A13, XXREAL_1:235; :: thesis:

end;

suppose A16: x in DYADIC ; :: thesis:

reconsider x = x as R_eal by XXREAL_0:def 1;
x <= b by A16, URYSOHN2:28, XXREAL_1:1;
hence contradiction by A13, XXREAL_1:235; :: thesis:

end;

end;

end;

the carrier of T c= the carrier of T ;
then reconsider s = the carrier of T as Subset of T ;
s = s ;
hence ex y being Subset of T st S₁[x,y] by A14; :: thesis:

end;

end;

end;

ex F being Function of DOM,(bool the carrier of T) st
for x being Element of DOM holds S₁[x,F . x] from FUNCT_2:sch 3(A2);
then consider F being Function of DOM,(bool the carrier of T) such that
A17: for x being Element of DOM holds S₁[x,F . x] ;
take F ; :: thesis:
thus for x being Real st x in DOM holds
( ( x in halfline 0 implies F . x = {} ) & ( x in right_open_halfline 1 implies F . x = the carrier of T ) & ( x in DYADIC implies for n being Nat st x in dyadic n holds
F . x = (G . n) . x ) ) by A17; :: thesis: