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] & not P _EQ_ O holds
(rep_pt P) `3_3 = 1
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] & not P _EQ_ O holds
(rep_pt P) `3_3 = 1
let P, O be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: ( O = [0,1,0] & not P _EQ_ O implies (rep_pt P) `3_3 = 1 )
assume A1: ( O = [0,1,0] & not P _EQ_ O ) ; :: thesis: (rep_pt P) `3_3 = 1
reconsider PP = P as Element of ProjCo (GF p) ;
P `3_3 <> 0 by A1, ThEQO;
then PP `3_3 <> 0 by EC_PF_2:32;
then rep_pt PP = [((PP `1_3) * ((PP `3_3) ")),((PP `2_3) * ((PP `3_3) ")),1] by EC_PF_2:def 7;
hence (rep_pt P) `3_3 = 1 by MCART_1:def 7; :: thesis: verum