let G1, G2 be Function of DOM,(bool the carrier of T); :: thesis:
assume that
A2: for x being Real st x in DOM holds
( ( x in halfline 0 implies G1 . x = {} ) & ( x in right_open_halfline 1 implies G1 . x = the carrier of T ) & ( x in DYADIC implies for n being Nat st x in dyadic n holds
G1 . x = (R . n) . x ) ) and
A3: for x being Real st x in DOM holds
( ( x in halfline 0 implies G2 . x = {} ) & ( x in right_open_halfline 1 implies G2 . x = the carrier of T ) & ( x in DYADIC implies for n being Nat st x in dyadic n holds
G2 . x = (R . n) . x ) ) ; :: thesis:
for x being object st x in DOM holds
G1 . x = G2 . x

proof

let x be object ; :: thesis:
assume A4: x in DOM ; :: thesis:
then reconsider x = x as Real ;
A5: ( x in (halfline 0) \/ DYADIC or x in right_open_halfline 1 ) by A4, URYSOHN1:def 3, XBOOLE_0:def 3;

per cases by A5, XBOOLE_0:def 3;

suppose A6: x in halfline 0 ; :: thesis:

then G1 . x = {} by A2, A4;
hence G1 . x = G2 . x by A3, A4, A6; :: thesis:

end;

suppose A7: x in right_open_halfline 1 ; :: thesis:

then G1 . x = the carrier of T by A2, A4;
hence G1 . x = G2 . x by A3, A4, A7; :: thesis:

end;

suppose A8: x in DYADIC ; :: thesis:

then consider n being Nat such that
A9: x in dyadic n by URYSOHN1:def 2;
G1 . x = (R . n) . x by A2, A4, A8, A9;
hence G1 . x = G2 . x by A3, A4, A8, A9; :: thesis:

end;

end;

end;

hence G1 = G2 by FUNCT_2:12; :: thesis: