let p be 5 _or_greater Prime; 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; 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); ( Q1 _EQ_ Q2 implies (addell_ProjCo (z,p)) . (P,Q1) _EQ_ (addell_ProjCo (z,p)) . (P,Q2) )
assume A1:
Q1 _EQ_ Q2
; (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; verum