:: deftheorem Def5 defines `3_3 EC_PF_2:def 5 :
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 `3_3 iff for px, py, pz being object st P = [px,py,pz] holds
b₅ = pz );