let G1, G2 be Function of T,R^1; :: thesis: ( ( for p being Point of T holds
( ( Rainbow (p,R) = {} implies G1 . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow (p,R) holds
G1 . p = sup S ) ) ) & ( for p being Point of T holds
( ( Rainbow (p,R) = {} implies G2 . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow (p,R) holds
G2 . p = sup S ) ) ) implies G1 = G2 )
assume that
A8: for p being Point of T holds
( ( Rainbow (p,R) = {} implies G1 . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow (p,R) holds
G1 . p = sup S ) ) and
A9: for p being Point of T holds
( ( Rainbow (p,R) = {} implies G2 . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow (p,R) holds
G2 . p = sup S ) ) ; :: thesis: G1 = G2
for x being object st x in the carrier of T holds
G1 . x = G2 . x
proof
let x be object ; :: thesis: ( x in the carrier of T implies G1 . x = G2 . x )
assume x in the carrier of T ; :: thesis: G1 . x = G2 . x
then reconsider x = x as Point of T ;
per cases ( Rainbow (x,R) = {} or Rainbow (x,R) <> {} ) ;
suppose A10: Rainbow (x,R) = {} ; :: thesis: G1 . x = G2 . x
then G1 . x = 0 by A8
.= G2 . x by A9, A10 ;
hence G1 . x = G2 . x ; :: thesis: verum
end;
suppose Rainbow (x,R) <> {} ; :: thesis: G1 . x = G2 . x
then reconsider S = Rainbow (x,R) as non empty Subset of ExtREAL ;
G1 . x = sup S by A8
.= G2 . x by A9 ;
hence G1 . x = G2 . x ; :: thesis: verum
end;
end;
end;
hence G1 = G2 by FUNCT_2:12; :: thesis: verum