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 A3, EC_PF_2:32;
then A5: rep_pt P = [0,1,0] by A3, EC_PF_2:def 7;
rep_pt O = [0,1,0] by A2, ThRepPoint5;
hence P _EQ_ O by A5, EC_PF_2:39; :: thesis: verum

end;

assume P _EQ_ O ; :: thesis: P `3_3 = 0
then rep_pt P = rep_pt O by EC_PF_2:39
.= O by A2, ThRepPoint5 ;
then (rep_pt PP) `3_3 = 0 by A2, A3, MCART_1:def 7;
then PP `3_3 = 0 by EC_PF_2:37;
hence P `3_3 = 0 by A3, EC_PF_2:32; :: thesis: verum