theorem Th20: :: EC_PF_1:20

for p being Prime
for a, b being Element of (GF p) holds
( ( a = 0 or b = 0 ) iff a * b = 0 )