for p being Prime
for a being Element of (GF p) holds
( a |^ 0 = 1_ (GF p) & a |^ 0 = 1 )