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

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