for R being Element of ProjCo (GF p) ex a being Element of (GF p) st
( a <> 0. (GF p) & R `1_3 = a * (R `1_3) & R `2_3 = a * (R `2_3) & R `3_3 = a * (R `3_3) )
proof
let R be Element of ProjCo (GF p); :: thesis: ex a being Element of (GF p) st
( a <> 0. (GF p) & R `1_3 = a * (R `1_3) & R `2_3 = a * (R `2_3) & R `3_3 = a * (R `3_3) )
reconsider a = 1. (GF p) as Element of (GF p) ;
( R `1_3 = a * (R `1_3) & R `2_3 = a * (R `2_3) & R `3_3 = a * (R `3_3) ) ;
hence ex a being Element of (GF p) st
( a <> 0. (GF p) & R `1_3 = a * (R `1_3) & R `2_3 = a * (R `2_3) & R `3_3 = a * (R `3_3) ) ; :: thesis: verum
end;
hence for P being Element of ProjCo (GF p) ex a being Element of (GF p) st
( a <> 0. (GF p) & P `1_3 = a * (P `1_3) & P `2_3 = a * (P `2_3) & P `3_3 = a * (P `3_3) ) ; :: thesis: verum