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

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

hence
G1 = G2
by FUNCT_2:12; :: thesis: verum
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 (halfline 0) \/ DYADIC or x in right_open_halfline 1 ) by A4, URYSOHN1:def 3, XBOOLE_0:def 3;

end;assume A4: x in DOM ; :: thesis: G1 . x = G2 . x

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;