:: deftheorem Def4 defines `2_3 EC_PF_2:def 4 :
for p being Prime
for a, b being Element of (GF p)
for P being Element of EC_SetProjCo (a,b,p)
for b<sub>5</sub> being Element of (GF p) holds
( b<sub>5</sub> = P `2_3 iff for px, py, pz being object st P = [px,py,pz] holds
b₅ = py );