theorem MOQ8: :: NEWTON06:60
for i being Integer holds
( (i |^ 4) mod 8 = 0 or (i |^ 4) mod 8 = 1 )