theorem Th31: :: EC_PF_2:31

for p being Prime
for a, b being Element of (GF p)
for P being Element of EC_SetProjCo (a,b,p) holds P = [(P `1_3),(P `2_3),(P `3_3)]