deffunc H₁( Element of 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 } ];
consider R being Function such that
A1: dom R = REAL and
A2: for x being Element of REAL holds R . x = H₁(x) from FUNCT_1:sch 4();
reconsider R = R as ManySortedSet of REAL by PARTFUN1:def 2, A1, RELAT_1:def 18;
take R ; :: thesis: for r being Real holds R . 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 } ]
let r be Real; :: thesis: R . 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 } ]
r in REAL by XREAL_0:def 1;
hence R . 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 } ] by A2; :: thesis: verum