let p be Prime; :: thesis: for a, b being Element of (GF p)
for P being Element of EC_SetProjCo (a,b,p) holds P = [(P `1_3),(P `2_3),(P `3_3)]
let a, b be Element of (GF p); :: thesis: for P being Element of EC_SetProjCo (a,b,p) holds P = [(P `1_3),(P `2_3),(P `3_3)]
let P be Element of EC_SetProjCo (a,b,p); :: thesis: P = [(P `1_3),(P `2_3),(P `3_3)]
P is Element of ProjCo (GF p) ;
then consider Px, Py, Pz being set such that
( Px in the carrier of (GF p) & Py in the carrier of (GF p) & Pz in the carrier of (GF p) ) and
A2: P = [Px,Py,Pz] by MCART_1:68;
thus P = [(P `1_3),Py,Pz] by A2, DefX
.= [(P `1_3),(P `2_3),Pz] by A2, DefY
.= [(P `1_3),(P `2_3),(P `3_3)] by A2, DefZ ; :: thesis: verum