:: deftheorem DefAffCompEll defines compell_AffCo EC_PF_3:def 2 :
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for b₃ being UnOp of (EC_SetAffCo (z,p)) holds
( b₃ = compell_AffCo (z,p) iff for P being Element of EC_SetAffCo (z,p) holds b₃ . P = rep_pt ((compell_ProjCo (z,p)) . P) );