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

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