let p be Prime; :: thesis: for a, b, d being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) holds
card { (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) } = 1 + (Lege_p (((d |^ 3) + (a * d)) + b))
let a, b, d be Element of (GF p); :: thesis: ( p > 3 & Disc (a,b,p) <> 0. (GF p) implies card { (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) } = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) )
assume AS: ( p > 3 & Disc (a,b,p) <> 0. (GF p) ) ; :: thesis: card { (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) } = 1 + (Lege_p (((d |^ 3) + (a * d)) + b))
set F = { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } ;
set 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) } ;

per cases ( { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } = {} or { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } <> {} ) ;

suppose NH2: { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } = {} ; :: thesis: card { (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) } = 1 + (Lege_p (((d |^ 3) + (a * d)) + b))

H1: { (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) } = {}

proof

assume { (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) } <> {} ; :: thesis: contradiction
then consider z being set such that
P1: z in { (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) } by XBOOLE_0:def 1;
consider Y being Element of (GF p) such that
P2: ( z = Class ((R_EllCur (a,b,p)),[d,Y,1]) & [d,Y,1] in EC_SetProjCo (a,b,p) ) by P1;
Y |^ 2 = ((d |^ 3) + (a * d)) + b by P2, ECAFF;
then Y in { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } ;
hence contradiction by NH2; :: thesis: verum

end;

2 < p by AS, XXREAL_0:2;
hence card { (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) } = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) by H1, NH2, QRRT1; :: thesis: verum

end;

suppose H2: { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } <> {} ; :: thesis: card { (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) } = 1 + (Lege_p (((d |^ 3) + (a * d)) + b))

then consider z being set such that
E0: z in { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } by XBOOLE_0:def 1;
consider W being Element of (GF p) such that
E1: ( z = W & W |^ 2 = ((d |^ 3) + (a * d)) + b ) by E0;
[d,W,1] is Element of EC_SetProjCo (a,b,p) by E1, ECAFF;
then H1: Class ((R_EllCur (a,b,p)),[d,W,1]) in { (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) } ;
consider I being Function of { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } , { (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) } such that
P0: ( I is onto & I is one-to-one ) by AS, H2, LmCardA;
A1: dom I = { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } by H1, FUNCT_2:def 1;
P2: rng I = { (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) } by P0, FUNCT_2:def 3;
then P1: card { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } c= card { (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) } by P0, A1, CARD_1:10;
reconsider h = I " as Function of { (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) } , { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } by P0, P2, FUNCT_2:25;
( (I ") * I = id { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } & I * (I ") = id { (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) } ) by P0, P2, H1, FUNCT_2:29;
then Q0: ( h is onto & h is one-to-one ) by FUNCT_2:23;
then Q1: rng h = { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } by FUNCT_2:def 3;
dom h = { (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) } by H2, FUNCT_2:def 1;
then card { (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) } c= card { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } by Q0, Q1, CARD_1:10;
then X1: card { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } = card { (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) } by P1, XBOOLE_0:def 10;
2 < p by AS, XXREAL_0:2;
hence card { (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) } = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) by X1, QRRT1; :: thesis: verum

end;

end;