let p be 5 _or_greater Prime; :: thesis: for z being Element of EC_WParam p
for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) st rep_pt P _EQ_ rep_pt Q holds
rep_pt P = rep_pt Q
let z be Element of EC_WParam p; :: thesis: for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) st rep_pt P _EQ_ rep_pt Q holds
rep_pt P = rep_pt Q
let P, Q be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: ( rep_pt P _EQ_ rep_pt Q implies rep_pt P = rep_pt Q )
assume A1: rep_pt P _EQ_ rep_pt Q ; :: thesis: rep_pt P = rep_pt Q
reconsider rP = rep_pt P, rQ = rep_pt Q as Element of EC_SetProjCo ((z `1),(z `2),p) by EC_PF_2:36;
rep_pt rP = rep_pt rQ by A1, EC_PF_2:39
.= rep_pt Q by LmRepPoint9 ;
hence rep_pt P = rep_pt Q by LmRepPoint9; :: thesis: verum