let p be Prime; :: thesis: for P, Q, R being Element of ProjCo (GF p) st P _EQ_ Q & Q _EQ_ R holds
P _EQ_ R
let P, Q, R be Element of ProjCo (GF p); :: thesis: ( P _EQ_ Q & Q _EQ_ R implies P _EQ_ R )
assume AS: ( P _EQ_ Q & Q _EQ_ R ) ; :: thesis: P _EQ_ R
then consider a being Element of (GF p) such that
P1: ( a <> 0. (GF p) & P `1 = a * (Q `1) & P `2 = a * (Q `2) & P `3 = a * (Q `3) ) by DefEQV;
consider b being Element of (GF p) such that
Q1: ( b <> 0. (GF p) & Q `1 = b * (R `1) & Q `2 = b * (R `2) & Q `3 = b * (R `3) ) by DefEQV, AS;
take d = a * b; :: according to EC_PF_1:def 10 :: thesis: ( d <> 0. (GF p) & P `1 = d * (R `1) & P `2 = d * (R `2) & P `3 = d * (R `3) )
thus ( d <> 0. (GF p) & P `1 = d * (R `1) & P `2 = d * (R `2) & P `3 = d * (R `3) ) by P1, Q1, GROUP_1:def 3, VECTSP_1:12; :: thesis: verum