let n be Nat; :: thesis: ( n is odd implies (n ^2) mod 8 = 1 )
assume n is odd ; :: thesis: (n ^2) mod 8 = 1
then ex a being Nat st n = (2 * a) + 1 by ABIAN:9;
hence (n ^2) mod 8 = 1 by Th36; :: thesis: verum