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