i ^2 = i |^ 2 by WSIERP_1:1;
hence (i ^2) + 1 is double_odd ; :: thesis: verum