A1: 2 |^ (2 + 1) = (2 |^ (1 + 1)) * 2 by NEWTON:6
.= ((2 |^ 1) * 2) * 2 by NEWTON:6 ;
A2: 2 |^ 3 divides a |^ 3 by NEWTON02:15, ABIAN:def 1;
a |^ (3 + 1) = (a |^ 3) * a by NEWTON:6;
then a |^ 3 divides a |^ (3 + 1) ;
then 8 divides a |^ 4 by A1, A2, INT_2:9;
hence (a |^ 4) mod 8 is zero by INT_1:62; :: thesis: verum