let p be 5 _or_greater Prime; :: thesis: for z being Element of EC_WParam p
for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) st P `3_3 <> 0 holds
( ( P `1_3 = Q `1_3 & P `3_3 = Q `3_3 ) iff ( P = Q or P = (compell_ProjCo (z,p)) . Q ) )
let z be Element of EC_WParam p; :: thesis: for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) st P `3_3 <> 0 holds
( ( P `1_3 = Q `1_3 & P `3_3 = Q `3_3 ) iff ( P = Q or P = (compell_ProjCo (z,p)) . Q ) )
let P, Q be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: ( P `3_3 <> 0 implies ( ( P `1_3 = Q `1_3 & P `3_3 = Q `3_3 ) iff ( P = Q or P = (compell_ProjCo (z,p)) . Q ) ) )
assume A1: P `3_3 <> 0 ; :: thesis: ( ( P `1_3 = Q `1_3 & P `3_3 = Q `3_3 ) iff ( P = Q or P = (compell_ProjCo (z,p)) . Q ) )
set a = z `1 ;
set b = z `2 ;
A2: P `3_3 <> 0. (GF p) by A1, EC_PF_1:11;

hereby :: thesis: ( ( P = Q or P = (compell_ProjCo (z,p)) . Q ) implies ( P `1_3 = Q `1_3 & P `3_3 = Q `3_3 ) )

assume A3: ( P `1_3 = Q `1_3 & P `3_3 = Q `3_3 ) ; :: thesis: ( P = Q or P = (compell_ProjCo (z,p)) . Q )
A4: (((P `2_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + (((z `1) * (P `1_3)) * ((P `3_3) |^ 2))) + ((z `2) * ((P `3_3) |^ 3))) = 0. (GF p) by Th35;
(((Q `2_3) |^ 2) * (Q `3_3)) - ((((Q `1_3) |^ 3) + (((z `1) * (Q `1_3)) * ((Q `3_3) |^ 2))) + ((z `2) * ((Q `3_3) |^ 3))) = 0. (GF p) by Th35;
then A5: ((Q `2_3) |^ 2) * (Q `3_3) = (((P `1_3) |^ 3) + (((z `1) * (P `1_3)) * ((Q `3_3) |^ 2))) + ((z `2) * ((P `3_3) |^ 3)) by A3, VECTSP_1:19
.= ((P `2_3) |^ 2) * (P `3_3) by A3, A4, VECTSP_1:19 ;
(P `2_3) * (P `2_3) = (P `2_3) |^ 2 by EC_PF_1:22
.= (Q `2_3) |^ 2 by A2, A3, A5, VECTSP_1:5
.= (Q `2_3) * (Q `2_3) by EC_PF_1:22 ;
then ( P `2_3 = Q `2_3 or P `2_3 = - (Q `2_3) ) by EC_PF_1:26;
then ( P = [(Q `1_3),(Q `2_3),(Q `3_3)] or P = [(Q `1_3),(- (Q `2_3)),(Q `3_3)] ) by A3, Th31;
hence ( P = Q or P = (compell_ProjCo (z,p)) . Q ) by Th31, Def8; :: thesis: verum

end;

assume A6: ( P = Q or P = (compell_ProjCo (z,p)) . Q ) ; :: thesis: ( P `1_3 = Q `1_3 & P `3_3 = Q `3_3 )
( P = [(Q `1_3),(Q `2_3),(Q `3_3)] or P = [(Q `1_3),(- (Q `2_3)),(Q `3_3)] ) by A6, Th31, Def8;
hence ( P `1_3 = Q `1_3 & P `3_3 = Q `3_3 ) by Def3, Def5; :: thesis: verum