theorem GP0: :: EC_PF_3:21

for p being 5 _or_greater Prime
for z being Element of EC_WParam p holds 1_ multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) = 0_EC (z,p)