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