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