P is Element of ProjCo (GF p) ;
then consider Px, Py, Pz being object such that
A11: ( Px in the carrier of (GF p) & Py in the carrier of (GF p) & Pz in the carrier of (GF p) ) and
A12: P = [Px,Py,Pz] by MCART_1:68;
take Pz ; :: thesis: ( Pz is set & Pz is Element of (GF p) & ( for px, py, pz being object st P = [px,py,pz] holds
Pz = pz ) )
thus ( Pz is set & Pz is Element of (GF p) & ( for px, py, pz being object st P = [px,py,pz] holds
Pz = pz ) ) by A11, A12, XTUPLE_0:3; :: thesis: verum