let p be 5 _or_greater Prime; for z being Element of EC_WParam p
for P, Q being Element of EC_SetAffCo (z,p) holds (addell_AffCo (z,p)) . (P,Q) = (addell_AffCo (z,p)) . (Q,P)
let z be Element of EC_WParam p; for P, Q being Element of EC_SetAffCo (z,p) holds (addell_AffCo (z,p)) . (P,Q) = (addell_AffCo (z,p)) . (Q,P)
let P, Q be Element of EC_SetAffCo (z,p); (addell_AffCo (z,p)) . (P,Q) = (addell_AffCo (z,p)) . (Q,P)
rep_pt ((addell_ProjCo (z,p)) . (P,Q)) =
rep_pt ((addell_ProjCo (z,p)) . (Q,P))
by ThCommutativeProjCo, EC_PF_2:39
.=
(addell_AffCo (z,p)) . (Q,P)
by DefAffAddEll
;
hence
(addell_AffCo (z,p)) . (P,Q) = (addell_AffCo (z,p)) . (Q,P)
by DefAffAddEll; verum