theorem ThAdd1: :: EC_PF_3:22

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