let x be Integer; :: thesis: for X being Subset of INT

for a being Integer holds

( x in a ** X iff ex y being Integer st

( y in X & x = a * y ) )

let X be Subset of INT; :: thesis: for a being Integer holds

( x in a ** X iff ex y being Integer st

( y in X & x = a * y ) )

let a be Integer; :: thesis: ( x in a ** X iff ex y being Integer st

( y in X & x = a * y ) )

reconsider x9 = x as Real ;

reconsider y = y as Real ;

ex z being Real st

( z in X & x9 = a * z ) by A3;

hence x in a ** X by MEMBER_1:193; :: thesis: verum

for a being Integer holds

( x in a ** X iff ex y being Integer st

( y in X & x = a * y ) )

let X be Subset of INT; :: thesis: for a being Integer holds

( x in a ** X iff ex y being Integer st

( y in X & x = a * y ) )

let a be Integer; :: thesis: ( x in a ** X iff ex y being Integer st

( y in X & x = a * y ) )

hereby :: thesis: ( ex y being Integer st

( y in X & x = a * y ) implies x in a ** X )

given y being Integer such that A3:
( y in X & x = a * y )
; :: thesis: x in a ** X( y in X & x = a * y ) implies x in a ** X )

assume
x in a ** X
; :: thesis: ex z being Integer st

( z in X & x = a * z )

then consider z being Complex such that

A1: x = a * z and

A2: z in X by MEMBER_1:195;

reconsider z = z as Integer by A2;

take z = z; :: thesis: ( z in X & x = a * z )

thus ( z in X & x = a * z ) by A2, A1; :: thesis: verum

end;( z in X & x = a * z )

then consider z being Complex such that

A1: x = a * z and

A2: z in X by MEMBER_1:195;

reconsider z = z as Integer by A2;

take z = z; :: thesis: ( z in X & x = a * z )

thus ( z in X & x = a * z ) by A2, A1; :: thesis: verum

reconsider x9 = x as Real ;

reconsider y = y as Real ;

ex z being Real st

( z in X & x9 = a * z ) by A3;

hence x in a ** X by MEMBER_1:193; :: thesis: verum