let X be real-membered set ; :: thesis: for a being real number holds X,a ++ X are_equipotent
let a be real number ; :: thesis: X,a ++ X are_equipotent
deffunc H₁( Real) -> Element of REAL = a + $1;
consider f being Function such that
A1: ( dom f = X & ( for x being Element of REAL st x in X holds
f . x = H₁(x) ) ) from GRAPH_5:sch 1();
take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & dom f = X & rng f = a ++ X )
A2: f is one-to-one

proof

let x, y be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume A3: ( x in dom f & y in dom f & f . x = f . y ) ; :: thesis: x = y
then ( x is real & y is real ) by A1;
then reconsider x = x, y = y as Real by XREAL_0:def 1;
( f . x = a + x & f . y = a + y ) by A1, A3;
then a + x = a + y by A3;
hence x = y ; :: thesis: verum

end;

rng f = a ++ X

proof

thus rng f c= a ++ X :: according to XBOOLE_0:def 10 :: thesis: a ++ X c= rng f

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng f or z in a ++ X )
assume z in rng f ; :: thesis: z in a ++ X
then consider x being set such that
A4: ( x in dom f & z = f . x ) by FUNCT_1:def 5;
reconsider x = x as real number by A1, A4;
reconsider x = x as Real by XREAL_0:def 1;
a + x is real ;
then reconsider z' = z as Real by A1, A4;
z' = a + x by A1, A4;
hence z in a ++ X by A1, A4, MEASURE6:def 6; :: thesis: verum

end;

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in a ++ X or z in rng f )
assume A5: z in a ++ X ; :: thesis: z in rng f
then reconsider z = z as Element of REAL ;
consider x being Real such that
A6: ( x in X & z = a + x ) by A5, MEASURE6:def 6;
reconsider x = x as Element of REAL ;
( f . x = z & x in dom f ) by A1, A6;
then consider x being Real such that
A7: ( x in dom f & z = f . x ) ;
thus z in rng f by A7, FUNCT_1:def 5; :: thesis: verum

end;

hence ( f is one-to-one & dom f = X & rng f = a ++ X ) by A1, A2; :: thesis: verum