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 A1: ( 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 A2: { 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))

A3: { (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 object such that
A4: 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
A5: ( z = Class ((R_EllCur (a,b,p)),[d,Y,1]) & [d,Y,1] in EC_SetProjCo (a,b,p) ) by A4;
Y |^ 2 = ((d |^ 3) + (a * d)) + b by A5, Th43;
then Y in { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } ;
hence contradiction by A2; :: thesis: verum

end;

2 < p by A1, 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 A3, A2, Th39; :: thesis: verum

end;

suppose A6: { 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 object such that
A7: 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
A8: ( z = W & W |^ 2 = ((d |^ 3) + (a * d)) + b ) by A7;
[d,W,1] is Element of EC_SetProjCo (a,b,p) by A8, Th43;
then A9: 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
A10: ( I is onto & I is one-to-one ) by A1, A6, Th58;
A11: dom I = { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } by A9, FUNCT_2:def 1;
A12: 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 A10, FUNCT_2:def 3;
then A13: 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 A10, A11, 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 A10, A12, 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 A10, A12, A9, FUNCT_2:29;
then A14: ( h is onto & h is one-to-one ) by FUNCT_2:23;
then A15: 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 A6, 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 A14, A15, CARD_1:10;
then A16: 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 A13, XBOOLE_0:def 10;
2 < p by A1, 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 A16, Th39; :: thesis: verum

end;

end;