let i be Integer; :: thesis: ( i is odd implies (i ^2) mod 8 = 1 )
assume i is odd ; :: thesis: (i ^2) mod 8 = 1
then ex j being Integer st i = (2 * j) + 1 by ABIAN:1;
hence (i ^2) mod 8 = 1 by Lm16; :: thesis: verum