consider k being Integer such that
A1: i = 2 * k by Lm1;
i * j = 2 * (k * j) by A1;
hence i * j is even ; :: thesis: verum