for p being Prime holds PrimeField (Z/ p) = Z/ p by EC_PF_1:def 2;