let p be Prime; :: thesis: for d, Y being Element of (GF p) holds [d,Y,1] is Element of ProjCo (GF p)
let d, Y be Element of (GF p); :: thesis: [d,Y,1] is Element of ProjCo (GF p)
set P = [d,Y,1];
[d,Y,1] <> [0,0,0] by XTUPLE_0:3;
then A1: not [d,Y,1] in {[0,0,0]} by TARSKI:def 1;
1. (GF p) in the carrier of (GF p) ;
then 1 in the carrier of (GF p) by Th12;
then [d,Y,1] in [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] by MCART_1:69;
then [d,Y,1] in [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] \ {[0,0,0]} by A1, XBOOLE_0:def 5;
hence [d,Y,1] is Element of ProjCo (GF p) by Th40; :: thesis: verum