let X be real-membered set ; :: thesis: for a being real number st a <> 0 holds
X,a ** X are_equipotent
let a be real number ; :: thesis: ( a <> 0 implies X,a ** X are_equipotent )
assume A1: a <> 0 ; :: thesis: X,a ** X are_equipotent
deffunc H₁( Real) -> Element of REAL = a * $1;
consider f being Function such that
A2: ( 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 )
A3: 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 A4: ( x in dom f & y in dom f & f . x = f . y ) ; :: thesis: x = y
then ( x is real & y is real ) by A2;
then reconsider x = x, y = y as Element of REAL by XREAL_0:def 1;
( f . x = a * x & f . y = a * y ) by A2, A4;
hence x = y by A1, A4, XCMPLX_1:5; :: 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
A5: ( x in dom f & z = f . x ) by FUNCT_1:def 5;
x is real by A2, A5;
then reconsider x' = x as Real by XREAL_0:def 1;
z = a * x' by A2, A5;
hence z in a ** X by A2, A5, INTEGRA2:def 2; :: thesis: verum

end;

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

end;

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