let p be Prime; :: thesis: for a, b being Element of (GF p)
for P being Element of EC_SetProjCo (a,b,p)
for Q being Element of ProjCo (GF p) holds
( P = Q iff ( P `1_3 = Q `1_3 & P `2_3 = Q `2_3 & P `3_3 = Q `3_3 ) )
let a, b be Element of (GF p); :: thesis: for P being Element of EC_SetProjCo (a,b,p)
for Q being Element of ProjCo (GF p) holds
( P = Q iff ( P `1_3 = Q `1_3 & P `2_3 = Q `2_3 & P `3_3 = Q `3_3 ) )
let P be Element of EC_SetProjCo (a,b,p); :: thesis: for Q being Element of ProjCo (GF p) holds
( P = Q iff ( P `1_3 = Q `1_3 & P `2_3 = Q `2_3 & P `3_3 = Q `3_3 ) )
let Q be Element of ProjCo (GF p); :: thesis: ( P = Q iff ( P `1_3 = Q `1_3 & P `2_3 = Q `2_3 & P `3_3 = Q `3_3 ) )
A2: P = [(P `1_3),(P `2_3),(P `3_3)] by ThECSet1;
A3: Q = [(Q `1_3),(Q `2_3),(Q `3_3)] by MCART_1:44;
thus ( P = Q implies ( P `1_3 = Q `1_3 & P `2_3 = Q `2_3 & P `3_3 = Q `3_3 ) ) by A2, A3, XTUPLE_0:3; :: thesis: ( P `1_3 = Q `1_3 & P `2_3 = Q `2_3 & P `3_3 = Q `3_3 implies P = Q )
assume A5: ( P `1_3 = Q `1_3 & P `2_3 = Q `2_3 & P `3_3 = Q `3_3 ) ; :: thesis: P = Q
thus P = Q by A3, A5, ThECSet1; :: thesis: verum