let p be Prime; :: thesis: for a, b being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) holds
ex F being FinSequence of NAT st
( len F = p & ( for n being Nat st n in Seg p holds
ex d being Element of (GF p) st
( d = n - 1 & F . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ) ) & card { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } = Sum F )
let a, b be Element of (GF p); :: thesis: ( p > 3 & Disc (a,b,p) <> 0. (GF p) implies ex F being FinSequence of NAT st
( len F = p & ( for n being Nat st n in Seg p holds
ex d being Element of (GF p) st
( d = n - 1 & F . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ) ) & card { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } = Sum F ) )
assume A1: ( p > 3 & Disc (a,b,p) <> 0. (GF p) ) ; :: thesis: ex F being FinSequence of NAT st
( len F = p & ( for n being Nat st n in Seg p holds
ex d being Element of (GF p) st
( d = n - 1 & F . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ) ) & card { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } = Sum F )
then consider S being Function such that
A2: ( dom S = Seg p & ( for n being Nat st n in dom S holds
S . n = { (Class ((R_EllCur (a,b,p)),[(n - 1),Y,1])) where Y is Element of (GF p) : [(n - 1),Y,1] in EC_SetProjCo (a,b,p) } ) & S is disjoint_valued & ( for n being Nat st n in dom S holds
S . n is finite ) & Union S = { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } ) by Lm8;
defpred S₁[ Nat, Nat] means $2 = card (S . $1);

A3: now :: thesis: for i being Nat st i in Seg p holds
ex x being Element of NAT st S₁[i,x]

let i be Nat; :: thesis: ( i in Seg p implies ex x being Element of NAT st S₁[i,x] )
assume i in Seg p ; :: thesis: ex x being Element of NAT st S₁[i,x]
then S . i is finite by A2;
then reconsider x = card (S . i) as Element of NAT by ORDINAL1:def 12;
take x = x; :: thesis: S₁[i,x]
thus S₁[i,x] ; :: thesis: verum

end;

consider L being FinSequence of NAT such that
A4: ( dom L = Seg p & ( for i being Nat st i in Seg p holds
S₁[i,L . i] ) ) from FINSEQ_1:sch 5(A3);
take L ; :: thesis: ( len L = p & ( for n being Nat st n in Seg p holds
ex d being Element of (GF p) st
( d = n - 1 & L . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ) ) & card { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } = Sum L )
p is Element of NAT by ORDINAL1:def 12;
hence len L = p by A4, FINSEQ_1:def 3; :: thesis: ( ( for n being Nat st n in Seg p holds
ex d being Element of (GF p) st
( d = n - 1 & L . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ) ) & card { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } = Sum L )

A5: now :: thesis: for n being Nat st n in Seg p holds
ex d being Element of (GF p) st
( d = n - 1 & L . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) )

let n be Nat; :: thesis: ( n in Seg p implies ex d being Element of (GF p) st
( d = n - 1 & L . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ) )
assume A6: n in Seg p ; :: thesis: ex d being Element of (GF p) st
( d = n - 1 & L . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) )
then ( 1 <= n & n <= p ) by FINSEQ_1:1;
then A7: ( 1 - 1 <= n - 1 & n - 1 <= p - 1 ) by XREAL_1:9;
then A8: n - 1 is Element of NAT by INT_1:3;
p - 1 < p - 0 by XREAL_1:15;
then n - 1 < p by A7, XXREAL_0:2;
then reconsider d = n - 1 as Element of (GF p) by A8, NAT_1:44;
take d = d; :: thesis: ( d = n - 1 & L . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) )
thus d = n - 1 ; :: thesis: L . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b))
thus L . n = card (S . n) by A4, A6
.= card { (Class ((R_EllCur (a,b,p)),[(n - 1),Y,1])) where Y is Element of (GF p) : [(n - 1),Y,1] in EC_SetProjCo (a,b,p) } by A2, A6
.= 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 Th59, A1 ; :: thesis: verum

end;

for i being Nat st i in dom S holds
( S . i is finite & L . i = card (S . i) ) by A2, A4;
hence ( ( for n being Nat st n in Seg p holds
ex d being Element of (GF p) st
( d = n - 1 & L . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ) ) & card { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } = Sum L ) by A2, A4, A5, DIST_1:17; :: thesis: verum