deffunc H₁( Real) -> set = Unique_No (sReal . $1);
let M1, M2 be ManySortedSet of REAL ; :: thesis: ( ( for r being Real holds M1 . r = Unique_No (sReal . r) ) & ( for r being Real holds M2 . r = Unique_No (sReal . r) ) 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