theorem Th8: :: NUMBER15:8
for m, n being Nat st ( ( n mod 4 = 1 & m mod 4 = 1 ) or ( n mod 4 = 3 & m mod 4 = 3 ) ) holds
(n * m) mod 4 = 1