let p be 5 _or_greater Prime; :: thesis: for z being Element of EC_WParam p
for P, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds
( P `3_3 = 0 iff P _EQ_ O )

let z be Element of EC_WParam p; :: thesis: for P, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds
( P `3_3 = 0 iff P _EQ_ O )

let P, O be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: ( O = [0,1,0] implies ( P `3_3 = 0 iff P _EQ_ O ) )
assume A2: O = [0,1,0] ; :: thesis: ( P `3_3 = 0 iff P _EQ_ O )
set a = z `1 ;
set b = z `2 ;
consider PP being Element of ProjCo (GF p) such that
A3: ( PP = P & PP in EC_SetProjCo ((z `1),(z `2),p) ) ;
hereby :: thesis: ( P _EQ_ O implies P `3_3 = 0 )
assume P `3_3 = 0 ; :: thesis: P _EQ_ O
then PP `3_3 = 0 by ;
then A5: rep_pt P = [0,1,0] by ;
rep_pt O = [0,1,0] by ;
hence P _EQ_ O by ; :: thesis: verum
end;
assume P _EQ_ O ; :: thesis:
then rep_pt P = rep_pt O by EC_PF_2:39
.= O by ;
then (rep_pt PP) `3_3 = 0 by ;
then PP `3_3 = 0 by EC_PF_2:37;
hence P `3_3 = 0 by ; :: thesis: verum