theorem :: EC_PF_1:61

for p being Prime
for a, b being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) holds
ex F being FinSequence of INT st
( len F = p & ( for n being Nat st n in Seg p holds
ex d being Element of (GF p) st
( d = n - 1 & F . n = Lege_p (((d |^ 3) + (a * d)) + b) ) ) & card (Class (R_EllCur (a,b,p))) = (1 + p) + (Sum F) )