theorem ThLeftZeroedAffCo: :: EC_PF_3:13

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