let y, z be Element of (GF p); :: thesis: ( ( for px, py, pz being object st P = [px,py,pz] holds
y = pz ) & ( for px, py, pz being object st P = [px,py,pz] holds
z = pz ) implies y = z )
assume A13: for px, py, pz being object st P = [px,py,pz] holds
y = pz ; :: thesis: ( ex px, py, pz being object st
( P = [px,py,pz] & not z = pz ) or y = z )
assume A14: for px, py, pz being object st P = [px,py,pz] holds
z = pz ; :: thesis: y = z
P is Element of ProjCo (GF p) ;
then consider Px, Py, Pz being object such that
( Px in the carrier of (GF p) & Py in the carrier of (GF p) & Pz in the carrier of (GF p) ) and
A15: P = [Px,Py,Pz] by MCART_1:68;
y = Pz by A13, A15;
hence y = z by A14, A15; :: thesis: verum