theorem Th9: :: NUMBER15:9

for m, n being Nat st ( ( n mod 4 = 1 & m mod 4 = 3 ) or ( n mod 4 = 3 & m mod 4 = 1 ) ) holds
(n * m) mod 4 = 3