for p being Prime
for a, b being Element of (GF p)
for P being Element of EC_SetProjCo (a,b,p) holds (((P `2_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3))) = 0. (GF p)