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) )
P1: 1 = 1. (GF p) by XLm3;
reconsider Q = [X,Y,1] as Element of ProjCo (GF p) by LMNGA0;
P2: Y |^ 2 = (Y |^ 2) * (1. (GF p)) by VECTSP_1:def 6;
P3: a * X = (a * X) * (1. (GF p)) by VECTSP_1:def 6
.= (a * X) * ((1. (GF p)) * (1. (GF p))) by VECTSP_1:def 6
.= (a * X) * ((1. (GF p)) |^ 2) by EXLm4 ;
P4: b = b * (1. (GF p)) by VECTSP_1:def 6
.= b * ((1. (GF p)) * (1. (GF p))) by VECTSP_1:def 6
.= b * ((1. (GF p)) |^ 2) by EXLm4
.= b * (((1. (GF p)) |^ 2) * (1. (GF p))) by VECTSP_1:def 6
.= b * ((1. (GF p)) |^ (2 + 1)) by EX5
.= 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 AS2: 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 AS2, VECTSP_1:19;
then (EC_WEqProjCo (a,b,p)) . Q = 0. (GF p) by P1, P2, P3, P4, LmECDefEQ;
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 P1, P2, P3, P4, LmECDefEQ;
hence Y |^ 2 = ((X |^ 3) + (a * X)) + b by VECTSP_1:19; :: thesis: verum