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 A1: ( 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 object such that
A2: z in F by A1, XBOOLE_0:def 1;
consider W being Element of (GF p) such that
A3: ( z = W & W |^ 2 = ((d |^ 3) + (a * d)) + b ) by A1, A2;
[d,W,1] is Element of EC_SetProjCo (a,b,p) by A3, Th43;
then A4: Class ((R_EllCur (a,b,p)),[d,W,1]) in G by A1;
deffunc H1( object ) -> Element of bool (EC_SetProjCo (a,b,p)) = Class ((R_EllCur (a,b,p)),[d,$1,1]);
A5: for x being object st x in F holds
H1(x) in G
proof
let x be object ; :: thesis: ( x in F implies H1(x) in G )
assume x in F ; :: thesis: H1(x) in G
then consider Y being Element of (GF p) such that
A6: ( x = Y & Y |^ 2 = ((d |^ 3) + (a * d)) + b ) by A1;
[d,Y,1] is Element of EC_SetProjCo (a,b,p) by A6, Th43;
hence H1(x) in G by A1, A6; :: thesis: verum
end;
consider I being Function of F,G such that
A7: for x being object st x in F holds
I . x = H1(x) from FUNCT_2:sch 2(A5);
 take I ; :: thesis: ( I is onto & I is one-to-one )
now :: thesis: for y being object st y in G holds
y in rng I
let y be object ; :: 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
A8: ( y = Class ((R_EllCur (a,b,p)),[d,P,1]) & [d,P,1] in EC_SetProjCo (a,b,p) ) by A1;
P |^ 2 = ((d |^ 3) + (a * d)) + b by A8, Th43;
then A9: P in F by A1;
then y = I . P by A7, A8;
hence y in rng I by A9, A4, FUNCT_2:112; :: thesis: verum
end;
then G c= rng I ;
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 :: thesis: for x1, x2 being object st x1 in dom I & x2 in dom I & I . x1 = I . x2 holds
x1 = x2
let x1, x2 be object ; :: thesis: ( x1 in dom I & x2 in dom I & I . x1 = I . x2 implies x1 = x2 )
assume A10: ( x1 in dom I & x2 in dom I & I . x1 = I . x2 ) ; :: thesis: x1 = x2
A11: ( x1 in F & x2 in F ) by A10;
then consider Y1 being Element of (GF p) such that
A12: ( x1 = Y1 & Y1 |^ 2 = ((d |^ 3) + (a * d)) + b ) by A1;
consider Y2 being Element of (GF p) such that
A13: ( x2 = Y2 & Y2 |^ 2 = ((d |^ 3) + (a * d)) + b ) by A1, A11;
A14: I . x1 = Class ((R_EllCur (a,b,p)),[d,x1,1]) by A10, A7;
A15: Class ((R_EllCur (a,b,p)),[d,x1,1]) = Class ((R_EllCur (a,b,p)),[d,x2,1]) by A10, A7, A14;
A16: [d,Y2,1] is Element of EC_SetProjCo (a,b,p) by Th43, A13;
[d,Y1,1] is Element of EC_SetProjCo (a,b,p) by Th43, A12;
hence x1 = x2 by A1, A12, A13, A15, A16, Th52; :: thesis: verum
end;
hence I is one-to-one by FUNCT_1:def 4; :: thesis: verum