:: deftheorem DefAffAddEll defines addell_AffCo EC_PF_3:def 3 :
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for b₃ being BinOp of (EC_SetAffCo (z,p)) holds
( b₃ = addell_AffCo (z,p) iff for P, Q being Element of EC_SetAffCo (z,p) holds b₃ . (P,Q) = rep_pt ((addell_ProjCo (z,p)) . (P,Q)) );