for p being Prime
for a, b being Element of (GF p) holds Lege_p (a * b) = (Lege_p a) * (Lege_p b)