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