theorem :: EC_PF_1:35

for p being Prime
for a being Element of (GF p) st a <> 0 holds
Lege_p (a |^ 2) = 1 by Th31, Th33;