theorem Th39: :: EC_PF_1:39

for p being Prime
for a being Element of (GF p) st 2 < p holds
card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a)