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

thus ( ex y being Integer st
( y in X & x = a * y ) implies x in a ** X ) by MEMBER_1:193; :: thesis: verum