consider k being Integer such that
A1: i = 2 * k by Def1;
consider l being Integer such that
A2: j = 2 * l by Def1;
i + j = 2 * (k + l) by A1, A2;
hence i + j is even ; :: thesis: verum