theorem ThUnityProjCo: :: EC_PF_3:12

for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds
( (addell_ProjCo (z,p)) . (P,O) _EQ_ P & (addell_ProjCo (z,p)) . (O,P) _EQ_ P )