let p be Prime; :: thesis: for a, b, X, Y being Element of (GF p) holds
( Y |^ 2 = ((X |^ 3) + (a * X)) + b iff [X,Y,1] is Element of EC_SetProjCo (a,b,p) )
let a, b, X, Y be Element of (GF p); :: thesis: ( Y |^ 2 = ((X |^ 3) + (a * X)) + b iff [X,Y,1] is Element of EC_SetProjCo (a,b,p) )
A1: 1 = 1. (GF p) by Th12;
reconsider Q = [X,Y,1] as Element of ProjCo (GF p) by Lm6;
A2: Y |^ 2 = (Y |^ 2) * (1. (GF p)) ;
A3: a * X = (a * X) * (1. (GF p))
.= (a * X) * ((1. (GF p)) * (1. (GF p)))
.= (a * X) * ((1. (GF p)) |^ 2) by Lm2 ;
A4: b = b * (1. (GF p))
.= b * ((1. (GF p)) * (1. (GF p)))
.= b * ((1. (GF p)) |^ 2) by Lm2
.= b * (((1. (GF p)) |^ 2) * (1. (GF p)))
.= b * ((1. (GF p)) |^ (2 + 1)) by Th24
.= b * ((1. (GF p)) |^ 3) ;

hereby :: thesis: ( [X,Y,1] is Element of EC_SetProjCo (a,b,p) implies Y |^ 2 = ((X |^ 3) + (a * X)) + b )

assume A5: Y |^ 2 = ((X |^ 3) + (a * X)) + b ; :: thesis: [X,Y,1] is Element of EC_SetProjCo (a,b,p)
(Y |^ 2) - (((X |^ 3) + (a * X)) + b) = 0. (GF p) by A5, VECTSP_1:19;
then (EC_WEqProjCo (a,b,p)) . Q = 0. (GF p) by A1, A2, A3, A4, Th41;
then Q in { P where P is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) } ;
hence [X,Y,1] is Element of EC_SetProjCo (a,b,p) ; :: thesis: verum

end;

assume [X,Y,1] is Element of EC_SetProjCo (a,b,p) ; :: thesis: Y |^ 2 = ((X |^ 3) + (a * X)) + b
then Q in { P where P is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) } ;
then ex P being Element of ProjCo (GF p) st
( P = Q & (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) ) ;
then (Y |^ 2) - (((X |^ 3) + (a * X)) + b) = 0. (GF p) by A1, A2, A3, A4, Th41;
hence Y |^ 2 = ((X |^ 3) + (a * X)) + b by VECTSP_1:19; :: thesis: verum