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