let a be odd Integer; :: thesis: (a |^ 4) mod 8 = 1
2 |^ (2 + 1) = (2 |^ (1 + 1)) * 2 by NEWTON:6
.= ((2 |^ 1) * 2) * 2 by NEWTON:6 ;
hence (a |^ 4) mod 8 = 1 by MOQ8; :: thesis: verum