let p be Prime; :: thesis: 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 )
let a, b, d be Element of (GF p); :: thesis: 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 )
let F, G be set ; :: thesis: ( 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) } implies ex I being Function of F,G st
( I is onto & I is one-to-one ) )
assume AS: ( 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,P,1])) where P is Element of (GF p) : [d,P,1] in EC_SetProjCo (a,b,p) } ) ; :: thesis: ex I being Function of F,G st
( I is onto & I is one-to-one )
consider z being set such that
E0: z in F by AS, XBOOLE_0:def 1;
consider W being Element of (GF p) such that
E1: ( z = W & W |^ 2 = ((d |^ 3) + (a * d)) + b ) by AS, E0;
[d,W,1] is Element of EC_SetProjCo (a,b,p) by E1, ECAFF;
then D0: Class ((R_EllCur (a,b,p)),[d,W,1]) in G by AS;
deffunc H₁( set ) -> Element of bool (EC_SetProjCo (a,b,p)) = Class ((R_EllCur (a,b,p)),[d,$1,1]);
P0: for x being set st x in F holds
H₁(x) in G

proof

let x be set ; :: thesis: ( x in F implies H₁(x) in G )
assume x in F ; :: thesis: H₁(x) in G
then consider Y being Element of (GF p) such that
P01: ( x = Y & Y |^ 2 = ((d |^ 3) + (a * d)) + b ) by AS;
[d,Y,1] is Element of EC_SetProjCo (a,b,p) by P01, ECAFF;
hence H₁(x) in G by AS, P01; :: thesis: verum

end;

consider I being Function of F,G such that
P1: for x being set st x in F holds
I . x = H₁(x) from FUNCT_2:sch 2(P0);
take I ; :: thesis: ( I is onto & I is one-to-one )

now

let y be set ; :: thesis: ( y in G implies y in rng I )
assume y in G ; :: thesis: y in rng I
then consider P being Element of (GF p) such that
D2: ( y = Class ((R_EllCur (a,b,p)),[d,P,1]) & [d,P,1] in EC_SetProjCo (a,b,p) ) by AS;
P |^ 2 = ((d |^ 3) + (a * d)) + b by D2, ECAFF;
then D3: P in F by AS;
then y = I . P by P1, D2;
hence y in rng I by D3, D0, FUNCT_2:112; :: thesis: verum

end;

then G c= rng I by TARSKI:def 3;
then G = rng I by XBOOLE_0:def 10;
hence I is onto by FUNCT_2:def 3; :: thesis: I is one-to-one

now

let x1, x2 be set ; :: thesis: ( x1 in dom I & x2 in dom I & I . x1 = I . x2 implies x1 = x2 )
assume AS2: ( x1 in dom I & x2 in dom I & I . x1 = I . x2 ) ; :: thesis: x1 = x2
Q1: ( x1 in F & x2 in F ) by AS2;
then consider Y1 being Element of (GF p) such that
P01: ( x1 = Y1 & Y1 |^ 2 = ((d |^ 3) + (a * d)) + b ) by AS;
consider Y2 being Element of (GF p) such that
P02: ( x2 = Y2 & Y2 |^ 2 = ((d |^ 3) + (a * d)) + b ) by AS, Q1;
P03: I . x1 = Class ((R_EllCur (a,b,p)),[d,x1,1]) by AS2, P1;
P05: Class ((R_EllCur (a,b,p)),[d,x1,1]) = Class ((R_EllCur (a,b,p)),[d,x2,1]) by AS2, P1, P03;
P08: [d,Y2,1] is Element of EC_SetProjCo (a,b,p) by ECAFF, P02;
[d,Y1,1] is Element of EC_SetProjCo (a,b,p) by ECAFF, P01;
hence x1 = x2 by AS, P01, P02, P05, P08, LMNGA2; :: thesis: verum

end;

hence I is one-to-one by FUNCT_1:def 4; :: thesis: verum