consider a being Integer such that
A1: i = (2 * a) + 1 by ABIAN:1;
i |^ 2 = i * i by WSIERP_1:1;
then (i |^ 2) + 1 = 2 * ((((2 * a) * a) + (2 * a)) + 1) by A1;
hence (i |^ 2) + 1 is double_odd ; :: thesis: verum