:: deftheorem Def8 defines compell_ProjCo EC_PF_2:def 8 :
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for b₃ being Function of (EC_SetProjCo ((z `1),(z `2),p)),(EC_SetProjCo ((z `1),(z `2),p)) holds
( b₃ = compell_ProjCo (z,p) iff for P being Element of EC_SetProjCo ((z `1),(z `2),p) holds b₃ . P = [(P `1_3),(- (P `2_3)),(P `3_3)] );