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 A1: ( 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
A2: ( 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 A3: dom S = Seg p by A2, 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 A2; :: 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 :: thesis: for x, y being object st x <> y holds
S . x misses S . y

let x, y be object ; :: thesis: ( x <> y implies S . b₁ misses S . b₂ )
assume A4: 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 A5: ( 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 A5, A2, FINSEQ_1:def 3;
then A6: ( n - 1 is Element of (GF p) & m - 1 is Element of (GF p) ) by Lm7;
A7: 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 A5, A2;
A8: 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 A5, A2;
thus S . x misses S . y :: thesis: verum

proof

assume S . x meets S . y ; :: thesis: contradiction
then consider z being object such that
A9: ( z in S . x & z in S . y ) by XBOOLE_0:3;
consider Yx being Element of (GF p) such that
A10: ( z = Class ((R_EllCur (a,b,p)),[(n - 1),Yx,1]) & [(n - 1),Yx,1] in EC_SetProjCo (a,b,p) ) by A7, A9;
consider Yy being Element of (GF p) such that
A11: ( z = Class ((R_EllCur (a,b,p)),[(m - 1),Yy,1]) & [(m - 1),Yy,1] in EC_SetProjCo (a,b,p) ) by A8, A9;
n - 1 = m - 1 by Th52, A1, A10, A11, A6;
hence contradiction by A4; :: 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 A12: n in dom S ; :: thesis: S . n is finite
then A13: 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 A2;
( 1 <= n & n <= p ) by A12, A3, FINSEQ_1:1;
then A14: ( 1 - 1 <= n - 1 & n - 1 <= p - 1 ) by XREAL_1:9;
then A15: n - 1 is Element of NAT by INT_1:3;
p - 1 < p - 0 by XREAL_1:15;
then n - 1 < p by A14, XXREAL_0:2;
then reconsider d = n - 1 as Element of (GF p) by A15, NAT_1:44;
A16: 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 A13
.= 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) by Th59, A1 ;
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 Def5;
hence 0 <= 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) ; :: thesis: verum

end;

suppose A17: ( ((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 :: thesis: 0 <= 1 + (Lege_p (((d |^ 3) + (a * d)) + b))

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

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 Def5;
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 Def5;
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 A16, 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 object 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 object ; :: 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
A18: ( x in Z & Z in rng S ) by TARSKI:def 4;
consider n being object such that
A19: ( n in dom S & Z = S . n ) by A18, FUNCT_1:def 3;
reconsider n = n as Nat by A19;
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 A19, A2;
then consider Y being Element of (GF p) such that
A20: ( x = Class ((R_EllCur (a,b,p)),[(n - 1),Y,1]) & [(n - 1),Y,1] in EC_SetProjCo (a,b,p) ) by A18, A19;
n - 1 is Element of (GF p) by A3, A19, Lm7;
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 A20; :: 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
A21: ( 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
A22: P = [X,Y,1] by A21;
reconsider n1 = X as Nat ;
A23: ( 0 <= n1 & n1 < p ) by NAT_1:44;
A24: 0 + 1 <= n1 + 1 by XREAL_1:6;
A25: n1 + 1 <= p by A23, NAT_1:13;
set n = n1 + 1;
A26: ( n1 + 1 in Seg p & (n1 + 1) - 1 = X ) by A24, A25;
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 A21, A22;
then A27: x in S . (n1 + 1) by A26, A2, A3;
S . (n1 + 1) in rng S by A26, A3, FUNCT_1:3;
hence x in union (rng S) by A27, 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:2; :: thesis: verum