theorem Th58: :: EC_PF_1:58

for p being Prime
for a, b, d being Element of (GF p)
for F, G being set st p > 3 & Disc (a,b,p) <> 0. (GF p) & F = { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } & F <> {} & G = { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } holds
ex I being Function of F,G st
( I is onto & I is one-to-one )