theorem Th1: :: IDEA_1:1

for i, j, k being Nat st j is prime & i < j & k < j & i <> 0 holds
ex a being Nat st
( (a * i) mod j = k & a < j )