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 INT 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 = Lege_p (((d |^ 3) + (a * d)) + b) ) ) & card (Class (R_EllCur (a,b,p))) = (1 + p) + (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 INT 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 = Lege_p (((d |^ 3) + (a * d)) + b) ) ) & card (Class (R_EllCur (a,b,p))) = (1 + p) + (Sum F) ) )
assume A1: ( p > 3 & Disc (a,b,p) <> 0. (GF p) ) ; :: thesis: ex F being FinSequence of INT 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 = Lege_p (((d |^ 3) + (a * d)) + b) ) ) & card (Class (R_EllCur (a,b,p))) = (1 + p) + (Sum F) )
then consider L being FinSequence of NAT such that
A2: ( 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 ) by Th60;
A3: p is Element of NAT by ORDINAL1:def 12;
defpred S₁[ Nat, set ] means ex d being Element of (GF p) st
( d = $1 - 1 & $2 = Lege_p (((d |^ 3) + (a * d)) + b) );

A4: now :: thesis: for n being Nat st n in Seg p holds
ex x being Element of INT st S₁[n,x]

let n be Nat; :: thesis: ( n in Seg p implies ex x being Element of INT st S₁[n,x] )
assume n in Seg p ; :: thesis: ex x being Element of INT st S₁[n,x]
then ( 1 <= n & n <= p ) by FINSEQ_1:1;
then A5: ( 1 - 1 <= n - 1 & n - 1 <= p - 1 ) by XREAL_1:9;
then A6: n - 1 is Element of NAT by INT_1:3;
p - 1 < p - 0 by XREAL_1:15;
then n - 1 < p by A5, XXREAL_0:2;
then reconsider d = n - 1 as Element of (GF p) by A6, NAT_1:44;
reconsider x = Lege_p (((d |^ 3) + (a * d)) + b) as Element of INT by INT_1:def 2;
take x = x; :: thesis: S₁[n,x]
thus S₁[n,x] ; :: thesis: verum

end;

consider F being FinSequence of INT such that
A7: ( dom F = Seg p & ( for i being Nat st i in Seg p holds
S₁[i,F . i] ) ) from FINSEQ_1:sch 5(A4);
take F ; :: thesis: ( 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 = Lege_p (((d |^ 3) + (a * d)) + b) ) ) & card (Class (R_EllCur (a,b,p))) = (1 + p) + (Sum F) )
thus A8: len F = p by A7, A3, 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 & F . n = Lege_p (((d |^ 3) + (a * d)) + b) ) ) & card (Class (R_EllCur (a,b,p))) = (1 + p) + (Sum F) )
reconsider pp = p |-> jj as Element of p -tuples_on REAL ;
F is FinSequence of REAL by FINSEQ_2:24, NUMBERS:15;
then reconsider FF = F as Element of p -tuples_on REAL by A8, FINSEQ_2:92;

A9: now :: thesis: for n being Nat st 1 <= n & n <= p holds
L . n = (pp + FF) . n

let n be Nat; :: thesis: ( 1 <= n & n <= p implies L . n = (pp + FF) . n )
assume ( 1 <= n & n <= p ) ; :: thesis: L . n = (pp + FF) . n
then A10: n in Seg p ;
then A11: ex d being Element of (GF p) st
( d = n - 1 & L . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ) by A2;
ex f being Element of (GF p) st
( f = n - 1 & F . n = Lege_p (((f |^ 3) + (a * f)) + b) ) by A7, A10;
then L . n = ((p |-> 1) . n) + (F . n) by A11, A10, FUNCOP_1:7;
hence L . n = (pp + FF) . n by RVSUM_1:11; :: thesis: verum

end;

len (pp + FF) = p by FINSEQ_2:132;
then L = pp + FF by A2, A9;
then Sum L = (Sum (p |-> 1)) + (Sum F) by RVSUM_1:89;
then A12: Sum L = (p * 1) + (Sum F) by RVSUM_1:80;
reconsider F1 = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} as finite set ;
reconsider F2 = { (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] ) } as finite set by A2;
A13: card F1 = 1 by CARD_2:42;
card (Class (R_EllCur (a,b,p))) = card (F1 \/ F2) by A1, Th51
.= 1 + (p + (Sum F)) by A1, A13, A2, A12, Th53, CARD_2:40 ;
hence ( ( for n being Nat st n in Seg p holds
ex d being Element of (GF p) st
( d = n - 1 & F . n = Lege_p (((d |^ 3) + (a * d)) + b) ) ) & card (Class (R_EllCur (a,b,p))) = (1 + p) + (Sum F) ) by A7; :: thesis: verum