let a be odd square Integer; :: thesis: a mod 8 = 1
((a - (((2 * 0) + 1) |^ 2)) mod 8) + (1 mod (1 + 7)) = 1 mod (1 + 7) by NEWTON05:22;
then ((a - 1) + 1) mod 8 = 1 by NAT_D:66;
hence a mod 8 = 1 ; :: thesis: verum