defpred S_{1}[ 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_{1}[x,y]

for x being Element of T holds S_{1}[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_{1}[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

$2 = sup S ) );

A1: for x being Element of T ex y being Element of R^1 st S

proof

ex F being Function of the carrier of T, the carrier of R^1 st
let x be Element of T; :: thesis: ex y being Element of R^1 st S_{1}[x,y]

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

end;

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

0 in REAL
by XREAL_0:def 1;

then reconsider y = 0 as Element of R^1 by TOPMETR:17;

S_{1}[x,y]
by A2;

hence ex y being Element of R^1 st S_{1}[x,y]
; :: thesis: verum

end;then reconsider y = 0 as Element of R^1 by TOPMETR:17;

S

hence ex y being Element of R^1 st S

suppose
Rainbow (x,R) <> {}
; :: thesis: ex y being Element of R^1 st S_{1}[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_{1}[x,y]

thus S_{1}[x,y]
; :: thesis: verum

end;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

thus S

for x being Element of T holds S

then consider F being Function of T,R^1 such that

A7: for x being Element of T holds S

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