let i, j be Integer; :: thesis: (i * j) gcd i = abs i
set a = (abs (i * j)) gcd (abs i);
E: abs i divides i by thabs0;
then D: abs i divides i * j by INT_2:2;
for m being Integer st m divides i * j & m divides i holds
m divides abs i

proof

let m be Integer; :: thesis: ( m divides i * j & m divides i implies m divides abs i )
assume ( m divides i * j & m divides i ) ; :: thesis: m divides abs i
then consider k being Integer such that
H: m * k = i by INT_1:def 9;
i divides abs i by thabs0;
then consider l being Integer such that
K: i * l = abs i by INT_1:def 9;
m * (k * l) = abs i by H, K;
hence m divides abs i by INT_1:def 9; :: thesis: verum

end;

hence (i * j) gcd i = abs i by D, E, INT_2:def 3; :: thesis: verum