let p be 5 _or_greater Prime; :: thesis: for z being Element of EC_WParam p
for P, Q1, Q2 being Element of EC_SetProjCo ((z `1),(z `2),p) st Q1 _EQ_ Q2 holds
(addell_ProjCo (z,p)) . (P,Q1) _EQ_ (addell_ProjCo (z,p)) . (P,Q2)
let z be Element of EC_WParam p; :: thesis: for P, Q1, Q2 being Element of EC_SetProjCo ((z `1),(z `2),p) st Q1 _EQ_ Q2 holds
(addell_ProjCo (z,p)) . (P,Q1) _EQ_ (addell_ProjCo (z,p)) . (P,Q2)
let P, Q1, Q2 be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: ( Q1 _EQ_ Q2 implies (addell_ProjCo (z,p)) . (P,Q1) _EQ_ (addell_ProjCo (z,p)) . (P,Q2) )
assume A1: Q1 _EQ_ Q2 ; :: thesis: (addell_ProjCo (z,p)) . (P,Q1) _EQ_ (addell_ProjCo (z,p)) . (P,Q2)
A2: (addell_ProjCo (z,p)) . (P,Q1) _EQ_ (addell_ProjCo (z,p)) . (Q1,P) by ThCommutativeProjCo;
(addell_ProjCo (z,p)) . (Q1,P) _EQ_ (addell_ProjCo (z,p)) . (Q2,P) by A1, ThAdd1;
then A3: (addell_ProjCo (z,p)) . (P,Q1) _EQ_ (addell_ProjCo (z,p)) . (Q2,P) by A2, EC_PF_1:44;
(addell_ProjCo (z,p)) . (Q2,P) _EQ_ (addell_ProjCo (z,p)) . (P,Q2) by ThCommutativeProjCo;
hence (addell_ProjCo (z,p)) . (P,Q1) _EQ_ (addell_ProjCo (z,p)) . (P,Q2) by A3, EC_PF_1:44; :: thesis: verum