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]

proof

let x be Element of T; :: thesis: ex y being Element of R^1 st S₁[x,y]

per cases ( Rainbow (x,R) = {} or Rainbow (x,R) <> {} ) ;

suppose A2: Rainbow (x,R) = {} ; :: thesis: ex y being Element of R^1 st S₁[x,y]

0 in REAL by XREAL_0:def 1;
then reconsider y = 0 as Element of R^1 by TOPMETR:17;
S₁[x,y] by A2;
hence ex y being Element of R^1 st S₁[x,y] ; :: thesis: verum

end;

suppose Rainbow (x,R) <> {} ; :: thesis: ex y being Element of R^1 st S₁[x,y]

then reconsider S = Rainbow (x,R) as non empty Subset of ExtREAL ;
reconsider e1 = 1 as R_eal by XXREAL_0:def 1;
consider q being object such that
A3: q in S by XBOOLE_0:def 1;
reconsider q = q as R_eal by A3;
A4: 0 in REAL by XREAL_0:def 1;
A5: 1 in REAL by XREAL_0:def 1;
S c= DYADIC by Th13;
then S c= [.0.,e1.] by URYSOHN2:28;
then A6: ( 0 <= inf S & sup S <= 1 ) by URYSOHN2:26;
( inf S <= q & q <= sup S ) by A3, XXREAL_2:3, XXREAL_2:4;
then sup S in REAL by A6, XXREAL_0:45, A4, A5;
then reconsider y = sup S as Element of R^1 by TOPMETR:17;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] ; :: thesis: verum

end;

end;

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: 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 ) )
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: verum