deffunc H₁( Real) -> Element of the carrier of (TOP-REAL 2) = |[$1,0]|;
consider f being Function such that
A1: dom f = REAL and
A2: for r being Element of REAL holds f . r = H₁(r) from FUNCT_1:sch 4();
REAL , y=0-line are_equipotent

proof

take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & proj1 f = REAL & proj2 f = y=0-line )
thus f is one-to-one :: thesis: ( proj1 f = REAL & proj2 f = y=0-line )

proof

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in proj1 f or not y in proj1 f or not f . x = f . y or x = y )
assume that
A3: x in dom f and
A4: y in dom f ; :: thesis: ( not f . x = f . y or x = y )
reconsider x = x, y = y as Element of REAL by A3, A4, A1;
A5: f . y = |[y,0]| by A2;
f . x = |[x,0]| by A2;
hence ( not f . x = f . y or x = y ) by A5, SPPOL_2:1; :: thesis: verum

end;

thus dom f = REAL by A1; :: thesis: proj2 f = y=0-line
thus rng f c= y=0-line :: according to XBOOLE_0:def 10 :: thesis: y=0-line c= proj2 f

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng f or a in y=0-line )
assume a in rng f ; :: thesis: a in y=0-line
then consider b being object such that
A6: b in dom f and
A7: a = f . b by FUNCT_1:def 3;
reconsider b = b as Element of REAL by A1, A6;
a = |[b,0]| by A2, A7;
hence a in y=0-line ; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in y=0-line or a in proj2 f )
assume A8: a in y=0-line ; :: thesis: a in proj2 f
then reconsider a = a as Point of (TOP-REAL 2) ;
reconsider a1 = a `1 as Element of REAL by XREAL_0:def 1;
A9: a = |[(a `1),(a `2)]| by EUCLID:53;
then a `2 = 0 by A8, Th15;
then a = f . a1 by A2, A9;
hence a in proj2 f by A1, FUNCT_1:def 3; :: thesis: verum

end;

hence card y=0-line = continuum by CARD_1:5, TOPGEN_3:def 4; :: thesis: verum