defpred S1[ 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 S1[x,y]
proof
let x be Element of T; :: thesis: ex y being Element of R^1 st S1[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 S1[x,y]
0 in REAL by XREAL_0:def 1;
then reconsider y = 0 as Element of R^1 by TOPMETR:17;
S1[x,y] by A2;
hence ex y being Element of R^1 st S1[x,y] ; :: thesis: verum
end;
suppose Rainbow (x,R) <> {} ; :: thesis: ex y being Element of R^1 st S1[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;
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 ;
then sup S in REAL by ;
then reconsider y = sup S as Element of R^1 by TOPMETR:17;
take y ; :: thesis: S1[x,y]
thus S1[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 S1[x,F . x] from then consider F being Function of T,R^1 such that
A7: for x being Element of T holds S1[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