:: deftheorem defines 0_EC EC_PF_3:def 4 :
for p being 5 _or_greater Prime
for z being Element of EC_WParam p holds 0_EC (z,p) = [0,1,0];