let y, z be Element of (GF p); :: thesis: ( ( for px, py, pz being object st P = [px,py,pz] holds
y = py ) & ( for px, py, pz being object st P = [px,py,pz] holds
z = py ) implies y = z )
assume A8: for px, py, pz being object st P = [px,py,pz] holds
y = py ; :: thesis: ( ex px, py, pz being object st
( P = [px,py,pz] & not z = py ) or y = z )
assume A9: for px, py, pz being object st P = [px,py,pz] holds
z = py ; :: 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
A10: P = [Px,Py,Pz] by MCART_1:68;
y = Py by A8, A10;
hence y = z by A9, A10; :: thesis: verum