for p being Prime
for a, b, Px, Py, Pz being Element of (GF p)
for P being Element of EC_SetProjCo (a,b,p) st P = [Px,Py,Pz] holds
( P `1_3 = Px & P `2_3 = Py & P `3_3 = Pz ) by Def3, Def4, Def5;