let p be 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)
let z be 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)
let P1, P2, Q1, Q2 be Element of EC_SetProjCo ((z `1),(z `2),p); ( P1 _EQ_ P2 & Q1 _EQ_ Q2 implies (addell_ProjCo (z,p)) . (P1,Q1) _EQ_ (addell_ProjCo (z,p)) . (P2,Q2) )
assume A1:
( P1 _EQ_ P2 & Q1 _EQ_ Q2 )
; (addell_ProjCo (z,p)) . (P1,Q1) _EQ_ (addell_ProjCo (z,p)) . (P2,Q2)
A2:
(addell_ProjCo (z,p)) . (P1,Q1) _EQ_ (addell_ProjCo (z,p)) . (P2,Q1)
by A1, ThAdd1;
(addell_ProjCo (z,p)) . (P2,Q1) _EQ_ (addell_ProjCo (z,p)) . (P2,Q2)
by A1, ThAdd2;
hence
(addell_ProjCo (z,p)) . (P1,Q1) _EQ_ (addell_ProjCo (z,p)) . (P2,Q2)
by A2, EC_PF_1:44; verum