let X be real-membered set ; :: thesis: for a being Real st a <> 0 holds
X,a ** X are_equipotent
let a be Real; :: thesis: ( a <> 0 implies 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();
assume A2: a <> 0 ; :: thesis: X,a ** X are_equipotent
A3: 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
A4: ( x in dom f & y in dom f ) and
A5: f . x = f . y ; :: thesis: x = y
reconsider x = x, y = y as Element of REAL by A1, A4, XREAL_0:def 1;
( f . x = a * x & f . y = a * y ) by A1, A4;
hence x = y by A2, A5, XCMPLX_1:5; :: thesis: verum

end;

take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & dom f = X & rng f = a ** X )
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
A6: x in dom f and
A7: z = f . x by FUNCT_1:def 3;
reconsider x9 = x as Element of REAL by A1, A6, XREAL_0:def 1;
z = a * x9 by A1, A6, A7;
hence z in a ** X by A1, A6, MEMBER_1:193; :: thesis: verum

end;

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in a ** X or z in rng f )
assume A8: z in a ** X ; :: thesis: z in rng f
then reconsider z = z as Element of REAL ;
consider x being Complex such that
A9: z = a * x and
A10: x in X by A8, MEMBER_1:195;
reconsider x = x as Element of REAL by A10, XREAL_0:def 1;
f . x = z by A1, A10, A9;
hence z in rng f by A1, A10, FUNCT_1:def 3; :: thesis: verum

end;

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