for p being Prime
for a, b being Element of (GF p)
for P being Element of ProjCo (GF p) st (rep_pt P) `3_3 <> 0 holds
( rep_pt P = [((P `1_3) * ((P `3_3) ")),((P `2_3) * ((P `3_3) ")),1] & P `3_3 <> 0 )