let n be Nat; :: thesis:
deffunc H₁( object ) -> Element of bool (bool the carrier of (TopSpaceMetr (Euclid n))) = OpenHypercubes (@ (object2RAT ($1,n)));
consider ff being Function such that
A1: dom ff = RAT n and
A2: for x being object st x in RAT n holds
ff . x = H₁(x) from FUNCT_1:sch 3();
A3: OpenHypercubesRAT n = rng ff

let x be object ; :: thesis:
assume x in OpenHypercubesRAT n ; :: thesis:
then consider q0 being Point of (Euclid n) such that
A4: x = OpenHypercubes q0 and
A5: q0 in RAT n ;
x = ff . q0

ff . q0 = H₁(q0) by A5, A2;
hence x = ff . q0 by A4, A5, Def1; :: thesis:

end;

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng ff ; :: thesis:
then consider q0 being object such that
A6: q0 in dom ff and
A7: x = ff . q0 by FUNCT_1:def 3;
( RAT n c= REAL n & q0 in RAT n ) by NUMBERS:12, Th5, A6, A1;
then reconsider q1 = q0 as Point of (Euclid n) ;
ff . q1 = H₁(q0) by A6, A1, A2;
hence x in OpenHypercubesRAT n by A7; :: thesis:

end;