let p be 5 _or_greater Prime; :: thesis: for z being Element of EC_WParam p
for P being Element of EC_SetProjCo ((z `1),(z `2),p) st P in EC_SetAffCo (z,p) holds
rep_pt P = P
let z be Element of EC_WParam p; :: thesis: for P being Element of EC_SetProjCo ((z `1),(z `2),p) st P in EC_SetAffCo (z,p) holds
rep_pt P = P
let P be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: ( P in EC_SetAffCo (z,p) implies rep_pt P = P )
assume P in EC_SetAffCo (z,p) ; :: thesis: rep_pt P = P
then X1: ex PP being Element of EC_SetProjCo ((z `1),(z `2),p) st
( P = PP & ( PP `3_3 = 1 or PP = [0,1,0] ) ) ;
reconsider PP = P as Element of ProjCo (GF p) ;
( PP = [0,1,0] or PP `3_3 = 1 ) by X1, EC_PF_2:32;
hence rep_pt P = P by ThRepPoint5; :: thesis: verum