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

hereby :: thesis: ( ex y being Integer st
( 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 Element of COMPLEX such that
A2: x = a * z and
A1: z in X by MEMBER_1:195;
reconsider z = z as Integer by A1;
take z = z; :: thesis: ( z in X & x = a * z )
thus ( z in X & x = a * z ) by A1, A2; :: thesis: verum

end;

given y being Integer such that A3: ( y in X & x = a * y ) ; :: thesis: x in a ** X
reconsider x9 = x as Real by XREAL_0:def 1;
reconsider y = y as Real by XREAL_0:def 1;
ex z being Real st
( z in X & x9 = a * z )

proof

take y ; :: thesis: ( y in X & x9 = a * y )
thus ( y in X & x9 = a * y ) by A3; :: thesis: verum

end;

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