:: deftheorem defines is_on_curve EC_PF_2:def 6 :
for p being Prime
for P being Element of ProjCo (GF p)
for CEQ being Function of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):],(GF p) holds
( P is_on_curve CEQ iff CEQ . P = 0. (GF p) );