let X be real-membered set ; :: thesis: for a being Real holds X,a ++ X are_equipotent
let a be Real; :: thesis: X,a ++ X are_equipotent
deffunc H₁( Real) -> set = 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 CLASSES1:sch 2();
A2: 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 object ; :: 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 object such that
A3: x in dom f and
A4: z = f . x by FUNCT_1:def 3;
reconsider x = x as Real by A1, A3;
reconsider x = x as Element of REAL by XREAL_0:def 1;
a + x in REAL by XREAL_0:def 1;
then reconsider z9 = z as Element of REAL by A1, A3, A4;
z9 = a + x by A1, A3, A4;
hence z in a ++ X by A1, A3, MEMBER_1:141; :: thesis: verum

end;

let z be object ; :: 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 Complex such that
A6: z = a + x and
A7: x in X by A5, MEMBER_1:143;
X c= REAL by MEMBERED:3;
then reconsider x = x as Element of REAL by A7;
f . x = z by A1, A7, A6;
hence z in rng f by A1, A7, FUNCT_1:def 3; :: thesis: verum

end;

take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & dom f = X & rng f = a ++ X )
f is one-to-one

proof

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume that
A8: x in dom f and
A9: y in dom f and
A10: f . x = f . y ; :: thesis: x = y
reconsider x = x, y = y as Element of REAL by A1, A8, A9, XREAL_0:def 1;
f . x = a + x by A1, A8;
then a + x = a + y by A1, A9, A10;
hence x = y ; :: thesis: verum

end;

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