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