theorem ThAddCompAffCo: :: EC_PF_3:16

for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P, O being Element of EC_SetAffCo (z,p) st O = [0,1,0] holds
(addell_AffCo (z,p)) . (P,((compell_AffCo (z,p)) . P)) = O