let G1, G2 be Function of DOM,(bool the carrier of T); :: thesis: ( ( 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 ) ) ) & ( 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 ) ) ) implies G1 = G2 )

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: G1 = G2
for x being object st x in DOM holds
G1 . x = G2 . x
proof
let x be object ; :: thesis: ( x in DOM implies G1 . x = G2 . x )
assume A4: x in DOM ; :: thesis: G1 . x = G2 . x
then reconsider x = x as Real ;
A5: ( x in () \/ DYADIC or x in right_open_halfline 1 ) by ;
per cases by ;
suppose A6: x in halfline 0 ; :: thesis: G1 . x = G2 . x
then G1 . x = {} by A2, A4;
hence G1 . x = G2 . x by A3, A4, A6; :: thesis: verum
end;
suppose A7: x in right_open_halfline 1 ; :: thesis: G1 . x = G2 . x
then G1 . x = the carrier of T by A2, A4;
hence G1 . x = G2 . x by A3, A4, A7; :: thesis: verum
end;
suppose A8: x in DYADIC ; :: thesis: G1 . x = G2 . x
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: verum
end;
end;
end;
hence G1 = G2 by FUNCT_2:12; :: thesis: verum