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_{1}( 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_{1}(x) ) )
from CLASSES1:sch 2();

A2: rng f = a ++ X

f is one-to-one

let a be Real; :: thesis: X,a ++ X are_equipotent

deffunc H

consider f being Function such that

A1: ( dom f = X & ( for x being Element of REAL st x in X holds

f . x = H

A2: rng f = a ++ X

proof

take
f
; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & dom f = X & rng f = a ++ X )
thus
rng f c= a ++ X
:: according to XBOOLE_0:def 10 :: thesis: a ++ X c= 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;proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in a ++ X or z in rng f )
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;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

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

f is one-to-one

proof

hence
( f is one-to-one & dom f = X & rng f = a ++ X )
by A1, A2; :: thesis: verum
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;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