theorem ThAdd3: :: EC_PF_3:24

for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P1, P2, Q1, Q2 being Element of EC_SetProjCo ((z `1),(z `2),p) st P1 _EQ_ P2 & Q1 _EQ_ Q2 holds
(addell_ProjCo (z,p)) . (P1,Q1) _EQ_ (addell_ProjCo (z,p)) . (P2,Q2)