let T be non empty TopSpace; :: thesis:
let A, B be Subset of T; :: thesis:
let R be Rain of A,B; :: thesis:
defpred S₁[ Element of T, set ] means ( ( Rainbow $1,R = {} implies $2 = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow $1,R holds
$2 = sup S ) );
A1: for x being Element of T ex y being Element of R^1 st S₁[x,y]

let x be Element of T; :: thesis:

per cases ;

suppose A2: Rainbow x,R = {} ; :: thesis:

reconsider y = 0 as Element of R^1 by TOPMETR:24;
S₁[x,y] by A2;
hence ex y being Element of R^1 st S₁[x,y] ; :: thesis:

end;

suppose Rainbow x,R <> {} ; :: thesis:

then reconsider S = Rainbow x,R as non empty Subset of ExtREAL ;
A3: S c= DYADIC by Th15;
reconsider e1 = 1 as R_eal by XXREAL_0:def 1;
S c= [.0. ,e1.] by A3, URYSOHN2:32, XBOOLE_1:1;
then A4: ( 0 <= inf S & sup S <= e1 ) by URYSOHN2:30;
consider q being set such that
A5: q in S by XBOOLE_0:def 1;
reconsider q = q as R_eal by A5;
( inf S <= q & q <= sup S ) by A5, XXREAL_2:3, XXREAL_2:4;
then reconsider y = sup S as Element of R^1 by A4, TOPMETR:24, XXREAL_0:45;
take y ; :: thesis:
thus S₁[x,y] ; :: thesis:

end;

ex F being Function of the carrier of T,the carrier of R^1 st
for x being Element of T holds S₁[x,F . x] from FUNCT_2:sch 3(A1);
then consider F being Function of T,R^1 such that
A7: for x being Element of T holds S₁[x,F . x] ;
take F ; :: thesis:
thus for p being Point of T holds
( ( Rainbow p,R = {} implies F . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow p,R holds
F . p = sup S ) ) by A7; :: thesis: