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] & rep_pt P _EQ_ O holds

( rep_pt P = O & 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] & rep_pt P _EQ_ O holds

( rep_pt P = O & P _EQ_ O )

let P, O be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: ( O = [0,1,0] & rep_pt P _EQ_ O implies ( rep_pt P = O & P _EQ_ O ) )

assume A1: ( O = [0,1,0] & rep_pt P _EQ_ O ) ; :: thesis: ( rep_pt P = O & P _EQ_ O )

reconsider rP = rep_pt P as Element of EC_SetProjCo ((z `1),(z `2),p) by EC_PF_2:36;

rP `3_3 = 0 by A1, ThEQO;

then (rep_pt P) `3_3 = 0 by EC_PF_2:32;

hence rep_pt P = O by A1, EC_PF_2:37; :: thesis: P _EQ_ O

then rep_pt P = rep_pt O by A1, ThRepPoint5;

hence P _EQ_ O by EC_PF_2:39; :: thesis: verum

for P, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] & rep_pt P _EQ_ O holds

( rep_pt P = O & 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] & rep_pt P _EQ_ O holds

( rep_pt P = O & P _EQ_ O )

let P, O be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: ( O = [0,1,0] & rep_pt P _EQ_ O implies ( rep_pt P = O & P _EQ_ O ) )

assume A1: ( O = [0,1,0] & rep_pt P _EQ_ O ) ; :: thesis: ( rep_pt P = O & P _EQ_ O )

reconsider rP = rep_pt P as Element of EC_SetProjCo ((z `1),(z `2),p) by EC_PF_2:36;

rP `3_3 = 0 by A1, ThEQO;

then (rep_pt P) `3_3 = 0 by EC_PF_2:32;

hence rep_pt P = O by A1, EC_PF_2:37; :: thesis: P _EQ_ O

then rep_pt P = rep_pt O by A1, ThRepPoint5;

hence P _EQ_ O by EC_PF_2:39; :: thesis: verum