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 AS: ( 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
P1: ( 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 LmECPFCardY;
X0: 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) );

P20: now

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 X2: ( 1 - 1 <= n - 1 & n - 1 <= p - 1 ) by XREAL_1:9;
then X3: n - 1 is Element of NAT by INT_1:3;
p - 1 < p - 0 by XREAL_1:15;
then n - 1 < p by X2, XXREAL_0:2;
then reconsider d = n - 1 as Element of (GF p) by X3, 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
P2: ( dom F = Seg p & ( for i being Nat st i in Seg p holds
S₁[i,F . i] ) ) from FINSEQ_1:sch 5(P20);
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 XX1: len F = p by P2, X0, 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 |-> 1 as Element of p -tuples_on REAL by FINSEQ_2:112;
F is FinSequence of REAL by FINSEQ_2:24, NUMBERS:15;
then reconsider FF = F as Element of p -tuples_on REAL by XX1, FINSEQ_2:92;

P3: now

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 P30: n in Seg p by FINSEQ_1:1;
then P31: ex d being Element of (GF p) st
( d = n - 1 & L . n = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ) by P1;
ex f being Element of (GF p) st
( f = n - 1 & F . n = Lege_p (((f |^ 3) + (a * f)) + b) ) by P2, P30;
then L . n = ((p |-> 1) . n) + (F . n) by P31, P30, FUNCOP_1:7;
hence L . n = (pp + FF) . n by RVSUM_1:11; :: thesis: verum

end;

len (pp + FF) = p by X0, FINSEQ_2:132;
then L = pp + FF by P1, P3, FINSEQ_1:14;
then Sum L = (Sum (p |-> 1)) + (Sum F) by RVSUM_1:89;
then P4: 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 P1;
F4: card F1 = 1 by CARD_2:42;
card (Class (R_EllCur (a,b,p))) = card (F1 \/ F2) by AS, LmDefREQ4
.= 1 + (p + (Sum F)) by AS, F4, P1, P4, MIS, 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 P2; :: thesis: verum