theorem :: EC_PF_1:22

for p being Prime
for a being Element of (GF p) holds a |^ 2 = a * a by Lm2;