theorem ThCommutativeAffCo: :: EC_PF_3:20

for p being 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)