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;

given y being Integer such that A3: ( y in X & x = a * y ) ; :: thesis: x in a ** X
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