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 A1: ( P _EQ_ Q & Q _EQ_ R ) ; :: thesis: P _EQ_ R
then consider a being Element of (GF p) such that
A2: ( 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) ) ;
consider b being Element of (GF p) such that
A3: ( b <> 0. (GF p) & Q `1_3 = b * (R `1_3) & Q `2_3 = b * (R `2_3) & Q `3_3 = b * (R `3_3) ) by A1;
take d = a * b; :: according to EC_PF_1:def 10 :: thesis: ( d <> 0. (GF p) & P `1_3 = d * (R `1_3) & P `2_3 = d * (R `2_3) & P `3_3 = d * (R `3_3) )
thus ( d <> 0. (GF p) & P `1_3 = d * (R `1_3) & P `2_3 = d * (R `2_3) & P `3_3 = d * (R `3_3) ) by A2, A3, GROUP_1:def 3, VECTSP_1:12; :: thesis: verum