deffunc H₁( Element of REAL ) -> set = Unique_No (sReal . $1);
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 = Unique_No (sReal . r)
let r be Real; :: thesis: R . r = Unique_No (sReal . r)
r in REAL by XREAL_0:def 1;
hence R . r = Unique_No (sReal . r) by A2; :: thesis: verum