deffunc H₁( Real) -> object = [ { (uDyadic . ([/(($1 * (2 |^ n)) - 1)\] / (2 |^ n))) where n is Nat : verum } , { (uDyadic . ([\(($1 * (2 |^ m)) + 1)/] / (2 |^ m))) where m is Nat : verum } ];
let M1, M2 be ManySortedSet of REAL ; :: thesis: ( ( for r being Real holds M1 . r = [ { (uDyadic . ([/((r * (2 |^ n)) - 1)\] / (2 |^ n))) where n is Nat : verum } , { (uDyadic . ([\((r * (2 |^ m)) + 1)/] / (2 |^ m))) where m is Nat : verum } ] ) & ( for r being Real holds M2 . r = [ { (uDyadic . ([/((r * (2 |^ n)) - 1)\] / (2 |^ n))) where n is Nat : verum } , { (uDyadic . ([\((r * (2 |^ m)) + 1)/] / (2 |^ m))) where m is Nat : verum } ] ) implies M1 = M2 )
assume that
A3: for r being Real holds M1 . r = H₁(r) and
A4: for r being Real holds M2 . r = H₁(r) ; :: thesis: M1 = M2
A5: ( dom M1 = REAL & REAL = dom M2 ) by PARTFUN1:def 2;
for o being object st o in REAL holds
M1 . o = M2 . o

proof

let o be object ; :: thesis: ( o in REAL implies M1 . o = M2 . o )
assume o in REAL ; :: thesis: M1 . o = M2 . o
then reconsider r = o as Real ;
M1 . o = H₁(r) by A3;
hence M1 . o = M2 . o by A4; :: thesis: verum

end;

hence M1 = M2 by A5, FUNCT_1:2; :: thesis: verum