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 ) )
A1: P = [(P `1_3),(P `2_3),(P `3_3)] by Th31;
A2: Q = [(Q `1_3),(Q `2_3),(Q `3_3)] by AA;
thus ( P = Q implies ( P `1_3 = Q `1_3 & P `2_3 = Q `2_3 & P `3_3 = Q `3_3 ) ) by A1; :: thesis: ( P `1_3 = Q `1_3 & P `2_3 = Q `2_3 & P `3_3 = Q `3_3 implies P = Q )
assume A3: ( 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 A2, A3, Th31; :: thesis: verum