let p be 5 _or_greater Prime; :: thesis: for P being Element of ProjCo (GF p) holds rep_pt (rep_pt P) = rep_pt P

let P be Element of ProjCo (GF p); :: thesis: rep_pt (rep_pt P) = rep_pt P

set rP = rep_pt P;

let P be Element of ProjCo (GF p); :: thesis: rep_pt (rep_pt P) = rep_pt P

set rP = rep_pt P;