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

( ( 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

hence
G1 = G2
by FUNCT_2:12; :: thesis: verum
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 ;

end;assume x in the carrier of T ; :: thesis: G1 . x = G2 . x

then reconsider x = x as Point of T ;