thus for P, Q being Element of ProjCo (GF p) st ex a being Element of (GF p) st
( a <> 0. (GF p) & P `1 = a * (Q `1) & P `2 = a * (Q `2) & P `3 = a * (Q `3) ) holds
ex b being Element of (GF p) st
( b <> 0. (GF p) & Q `1 = b * (P `1) & Q `2 = b * (P `2) & Q `3 = b * (P `3) ) :: thesis: verum

proof

let P, Q be Element of ProjCo (GF p); :: thesis: ( ex a being Element of (GF p) st
( a <> 0. (GF p) & P `1 = a * (Q `1) & P `2 = a * (Q `2) & P `3 = a * (Q `3) ) implies ex b being Element of (GF p) st
( b <> 0. (GF p) & Q `1 = b * (P `1) & Q `2 = b * (P `2) & Q `3 = b * (P `3) ) )
given 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) ) ; :: thesis: ex b being Element of (GF p) st
( b <> 0. (GF p) & Q `1 = b * (P `1) & Q `2 = b * (P `2) & Q `3 = b * (P `3) )
take b = a " ; :: thesis: ( b <> 0. (GF p) & Q `1 = b * (P `1) & Q `2 = b * (P `2) & Q `3 = b * (P `3) )
P2: b <> 0. (GF p)

proof

assume b = 0. (GF p) ; :: thesis: contradiction
then b * a = 0. (GF p) by VECTSP_1:7;
then 1. (GF p) = 0. (GF p) by P1, VECTSP_1:def 10;
hence contradiction ; :: thesis: verum

end;

P3: Q `1 = (1. (GF p)) * (Q `1) by VECTSP_1:def 6
.= (b * a) * (Q `1) by P1, VECTSP_1:def 10
.= b * (P `1) by P1, GROUP_1:def 3 ;
P4: Q `2 = (1. (GF p)) * (Q `2) by VECTSP_1:def 6
.= (b * a) * (Q `2) by P1, VECTSP_1:def 10
.= b * (P `2) by P1, GROUP_1:def 3 ;
Q `3 = (1. (GF p)) * (Q `3) by VECTSP_1:def 6
.= (b * a) * (Q `3) by P1, VECTSP_1:def 10
.= b * (P `3) by P1, GROUP_1:def 3 ;
hence ( b <> 0. (GF p) & Q `1 = b * (P `1) & Q `2 = b * (P `2) & Q `3 = b * (P `3) ) by P2, P3, P4; :: thesis: verum

end;