let p be Prime; :: thesis: for a, b, c, d being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) holds
ex S being Function st
( 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] ) } )
let a, b, c, d be Element of (GF p); :: thesis: ( p > 3 & Disc (a,b,p) <> 0. (GF p) implies ex S being Function st
( 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] ) } ) )
assume AS: ( p > 3 & Disc (a,b,p) <> 0. (GF p) ) ; :: thesis: ex S being Function st
( 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] ) } )
deffunc H₁( Nat) -> set = { (Class ((R_EllCur (a,b,p)),[($1 - 1),Y,1])) where Y is Element of (GF p) : [($1 - 1),Y,1] in EC_SetProjCo (a,b,p) } ;
consider S being FinSequence such that
P2: ( len S = p & ( for i being Nat st i in dom S holds
S . i = H₁(i) ) ) from FINSEQ_1:sch 2();
take S ; :: thesis: ( 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] ) } )
thus P20: dom S = Seg p by P2, FINSEQ_1:def 3; :: thesis: ( ( 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] ) } )
thus 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) } by P2; :: thesis: ( 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] ) } )

now

let x, y be set ; :: thesis: ( x <> y implies S . b₁ misses S . b₂ )
assume A3: x <> y ; :: thesis: S . b₁ misses S . b₂

per cases ( ( x in dom S & y in dom S ) or not x in dom S or not y in dom S ) ;

suppose A4: ( x in dom S & y in dom S ) ; :: thesis: S . b₁ misses S . b₂

then reconsider n = x, m = y as Nat ;
( x in Seg p & y in Seg p ) by A4, P2, FINSEQ_1:def 3;
then V1: ( n - 1 is Element of (GF p) & m - 1 is Element of (GF p) ) by LMNG;
A40: 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) } by A4, P2;
A41: S . m = { (Class ((R_EllCur (a,b,p)),[(m - 1),Y,1])) where Y is Element of (GF p) : [(m - 1),Y,1] in EC_SetProjCo (a,b,p) } by A4, P2;
thus S . x misses S . y :: thesis: verum

proof

assume S . x meets S . y ; :: thesis: contradiction
then consider z being set such that
A50: ( z in S . x & z in S . y ) by XBOOLE_0:3;
consider Yx being Element of (GF p) such that
A52: ( z = Class ((R_EllCur (a,b,p)),[(n - 1),Yx,1]) & [(n - 1),Yx,1] in EC_SetProjCo (a,b,p) ) by A40, A50;
consider Yy being Element of (GF p) such that
A53: ( z = Class ((R_EllCur (a,b,p)),[(m - 1),Yy,1]) & [(m - 1),Yy,1] in EC_SetProjCo (a,b,p) ) by A41, A50;
n - 1 = m - 1 by LMNGA2, AS, A52, A53, V1;
hence contradiction by A3; :: thesis: verum

end;

end;

suppose ( not x in dom S or not y in dom S ) ; :: thesis: S . b₁ misses S . b₂

then ( S . x = {} or S . y = {} ) by FUNCT_1:def 2;
hence S . x misses S . y by XBOOLE_1:65; :: thesis: verum

end;

end;

end;

hence S is disjoint_valued by PROB_2:def 2; :: thesis: ( ( 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] ) } )
thus for n being Nat st n in dom S holds
S . n is finite :: thesis: 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] ) }

proof

let n be Nat; :: thesis: ( n in dom S implies S . n is finite )
assume ASN: n in dom S ; :: thesis: S . n is finite
then Q1: 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) } by P2;
( 1 <= n & n <= p ) by ASN, P20, 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;
X1: card (S . n) = 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 Q1
.= 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) by LmECPFCardB, AS ;
0 <= 1 + (Lege_p (((d |^ 3) + (a * d)) + b))

proof

per cases ( ( not ((d |^ 3) + (a * d)) + b = 0 & not ((d |^ 3) + (a * d)) + b is quadratic_residue ) or ((d |^ 3) + (a * d)) + b = 0 or ((d |^ 3) + (a * d)) + b is quadratic_residue ) ;

suppose ( not ((d |^ 3) + (a * d)) + b = 0 & not ((d |^ 3) + (a * d)) + b is quadratic_residue ) ; :: thesis: 0 <= 1 + (Lege_p (((d |^ 3) + (a * d)) + b))

then Lege_p (((d |^ 3) + (a * d)) + b) = - 1 by QRDef3;
hence 0 <= 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ; :: thesis: verum

end;

suppose C2: ( ((d |^ 3) + (a * d)) + b = 0 or ((d |^ 3) + (a * d)) + b is quadratic_residue ) ; :: thesis: 0 <= 1 + (Lege_p (((d |^ 3) + (a * d)) + b))

now

per cases ( ((d |^ 3) + (a * d)) + b = 0 or ((d |^ 3) + (a * d)) + b is quadratic_residue ) by C2;

suppose ((d |^ 3) + (a * d)) + b = 0 ; :: thesis: 0 <= 1 + (Lege_p (((d |^ 3) + (a * d)) + b))

then Lege_p (((d |^ 3) + (a * d)) + b) = 0 by QRDef3;
hence 0 <= 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ; :: thesis: verum

end;

suppose ((d |^ 3) + (a * d)) + b is quadratic_residue ; :: thesis: 0 <= 1 + (Lege_p (((d |^ 3) + (a * d)) + b))

then Lege_p (((d |^ 3) + (a * d)) + b) = 1 by QRDef3;
hence 0 <= 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ; :: thesis: verum

end;

end;

end;

hence 0 <= 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ; :: thesis: verum

end;

end;

end;

then card (S . n) in NAT by X1, INT_1:3;
hence S . n is finite ; :: thesis: verum

end;

set B = { (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] ) } ;
for x being set holds
( x in union (rng S) iff x in { (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] ) } )

proof

let x be set ; :: thesis: ( x in union (rng S) iff x in { (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] ) } )

hereby :: thesis: ( x in { (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] ) } implies x in union (rng S) )

assume x in union (rng S) ; :: thesis: x in { (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] ) }
then consider Z being set such that
A2: ( x in Z & Z in rng S ) by TARSKI:def 4;
consider n being set such that
A4: ( n in dom S & Z = S . n ) by A2, FUNCT_1:def 3;
reconsider n = n as Nat by A4;
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) } by A4, P2;
then consider Y being Element of (GF p) such that
A6: ( x = Class ((R_EllCur (a,b,p)),[(n - 1),Y,1]) & [(n - 1),Y,1] in EC_SetProjCo (a,b,p) ) by A2, A4;
n - 1 is Element of (GF p) by P20, A4, LMNG;
hence x in { (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 A6; :: thesis: verum

end;

assume x in { (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] ) } ; :: thesis: x in union (rng S)
then consider P being Element of ProjCo (GF p) such that
A3: ( x = Class ((R_EllCur (a,b,p)),P) & P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) ;
consider X, Y being Element of (GF p) such that
A4: P = [X,Y,1] by A3;
reconsider n1 = X as Nat ;
D2: ( 0 <= n1 & n1 < p ) by NAT_1:44;
D3: 0 + 1 <= n1 + 1 by XREAL_1:6;
D4: n1 + 1 <= p by D2, NAT_1:13;
set n = n1 + 1;
A5: ( n1 + 1 in Seg p & (n1 + 1) - 1 = X ) by D3, D4;
x in { (Class ((R_EllCur (a,b,p)),[((n1 + 1) - 1),Q,1])) where Q is Element of (GF p) : [((n1 + 1) - 1),Q,1] in EC_SetProjCo (a,b,p) } by A3, A4;
then A6: x in S . (n1 + 1) by A5, P2, P20;
S . (n1 + 1) in rng S by A5, P20, FUNCT_1:3;
hence x in union (rng S) by A6, TARSKI:def 4; :: thesis: verum

end;

hence 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 TARSKI:1; :: thesis: verum