let p be 5 _or_greater Prime; :: thesis: 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; :: thesis: 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); :: thesis: ( 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 ) ; :: thesis: (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; :: thesis: verum