:: deftheorem Def7 defines rep_pt EC_PF_2:def 7 :
for p being Prime
for P being Element of ProjCo (GF p) holds
( ( P `3_3 <> 0 implies rep_pt P = [((P `1_3) * ((P `3_3) ")),((P `2_3) * ((P `3_3) ")),1] ) & ( P `3_3 = 0 implies rep_pt P = [0,1,0] ) );