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_{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();

assume A2: a <> 0 ; :: thesis: X,a ** X are_equipotent

A3: f is one-to-one

rng f = a ** X

X,a ** X are_equipotent

let a be Real; :: thesis: ( a <> 0 implies 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

assume A2: a <> 0 ; :: thesis: X,a ** X are_equipotent

A3: f is one-to-one

proof

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

rng f = a ** X

proof

hence
( f is one-to-one & dom f = X & rng f = a ** X )
by A1, A3; :: thesis: verum
thus
rng f c= a ** X
:: according to XBOOLE_0:def 10 :: thesis: a ** X c= 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;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

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;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

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