let p be Prime; :: thesis: for a, b, X, Y, Z being Element of (GF p) holds (EC_WEqProjCo (a,b,p)) . [X,Y,Z] = ((Y |^ 2) * Z) - (((X |^ 3) + ((a * X) * (Z |^ 2))) + (b * (Z |^ 3)))
let a, b be Element of (GF p); :: thesis: for X, Y, Z being Element of (GF p) holds (EC_WEqProjCo (a,b,p)) . [X,Y,Z] = ((Y |^ 2) * Z) - (((X |^ 3) + ((a * X) * (Z |^ 2))) + (b * (Z |^ 3)))
let X, Y, Z be Element of (GF p); :: thesis: (EC_WEqProjCo (a,b,p)) . [X,Y,Z] = ((Y |^ 2) * Z) - (((X |^ 3) + ((a * X) * (Z |^ 2))) + (b * (Z |^ 3)))
set DX = [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):];
reconsider P = [X,Y,Z] as Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] ;
( P `1_3 = X & P `2_3 = Y & P `3_3 = Z ) ;
hence (EC_WEqProjCo (a,b,p)) . [X,Y,Z] = ((Y |^ 2) * Z) - (((X |^ 3) + ((a * X) * (Z |^ 2))) + (b * (Z |^ 3))) by Def8; :: thesis: verum