let p be Prime; 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); 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); 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
; verum