theorem ThRightZeroedAffCo: :: EC_PF_3:14

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,O) = P