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;

per cases ( P `3_3 = 0 or P `3_3 <> 0 ) ;

suppose A1: P `3_3 = 0 ; :: thesis: rep_pt (rep_pt P) = rep_pt P

then rep_pt P = [0,1,0] by EC_PF_2:def 7;
then (rep_pt P) `3_3 = 0 by MCART_1:def 7;
hence rep_pt (rep_pt P) = [0,1,0] by EC_PF_2:def 7
.= rep_pt P by A1, EC_PF_2:def 7 ;
:: thesis: verum

end;

suppose P `3_3 <> 0 ; :: thesis: rep_pt (rep_pt P) = rep_pt P

then rep_pt P = [((P `1_3) * ((P `3_3) ")),((P `2_3) * ((P `3_3) ")),1] by EC_PF_2:def 7;
then (rep_pt P) `3_3 = 1 by MCART_1:def 7;
hence rep_pt (rep_pt P) = rep_pt P by ThRepPoint5; :: thesis: verum

end;

end;