:: deftheorem Def10 defines _EQ_ EC_PF_1:def 10 :
for p being Prime
for P, Q being Element of ProjCo (GF p) holds
( P _EQ_ Q iff ex a being Element of (GF p) st
( a <> 0. (GF p) & P `1_3 = a * (Q `1_3) & P `2_3 = a * (Q `2_3) & P `3_3 = a * (Q `3_3) ) );