theorem Th20: :: NAT_5:20

for l, p, n1, n2 being Nat st 0 <> l & p > l & p > n1 & p > n2 & (l * n1) mod p = (l * n2) mod p & p is prime holds
n1 = n2