let T be non empty TopSpace; :: thesis: for A, B being Subset of T
for R being Rain of A,B ex F being Function of T,R^1 st
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 ) )
let A, B be Subset of T; :: thesis: for R being Rain of A,B ex F being Function of T,R^1 st
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 ) )
let R be Rain of A,B; :: thesis: ex F being Function of T,R^1 st
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 ) )
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]

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: 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 set such that
A3: q in S by XBOOLE_0:def 1;
reconsider q = q as R_eal by A3;
S c= DYADIC by Th15;
then S c= [.0. ,e1.] by URYSOHN2:32, XBOOLE_1:1;
then A4: ( 0 <= inf S & sup S <= e1 ) by URYSOHN2:30;
( inf S <= q & q <= sup S ) by A3, 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: 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
A5: 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 A5; :: thesis: verum