let p be Prime; :: thesis: for P, Q being Element of ProjCo (GF p) holds
( P _EQ_ Q iff [P,Q] in R_ProjCo p )
let P, Q be Element of ProjCo (GF p); :: thesis: ( P _EQ_ Q iff [P,Q] in R_ProjCo p )
thus ( P _EQ_ Q implies [P,Q] in R_ProjCo p ) ; :: thesis: ( [P,Q] in R_ProjCo p implies P _EQ_ Q )
assume [P,Q] in R_ProjCo p ; :: thesis: P _EQ_ Q
then consider X0, Y0 being Element of ProjCo (GF p) such that
A1: ( [P,Q] = [X0,Y0] & X0 _EQ_ Y0 ) ;
( P = X0 & Q = Y0 ) by A1, XTUPLE_0:1;
hence P _EQ_ Q by A1; :: thesis: verum