theorem LmRepPoint9: :: EC_PF_3:10

for p being 5 _or_greater Prime
for P being Element of ProjCo (GF p) holds rep_pt (rep_pt P) = rep_pt P