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 object such that
( Px in the carrier of (GF p) & Py in the carrier of (GF p) & Pz in the carrier of (GF p) ) and
A1: P = [Px,Py,Pz] by MCART_1:68;
thus P = [(P `1_3),Py,Pz] by A1, Def3
.= [(P `1_3),(P `2_3),Pz] by A1, Def4
.= [(P `1_3),(P `2_3),(P `3_3)] by A1, Def5 ; :: thesis: verum