for p being Prime
for a, b being Element of (GF p)
for P being Element of EC_SetProjCo (a,b,p)
for Q being Element of ProjCo (GF p) holds
( P = Q iff ( P `1_3 = Q `1_3 & P `2_3 = Q `2_3 & P `3_3 = Q `3_3 ) )