let p be Prime; :: thesis: for a, b being Element of (GF p)
for P, Q being Element of ProjCo (GF p) st Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & Q in EC_SetProjCo (a,b,p) holds
( P _EQ_ Q iff [P,Q] in R_EllCur (a,b,p) )
let a, b be Element of (GF p); :: thesis: for P, Q being Element of ProjCo (GF p) st Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & Q in EC_SetProjCo (a,b,p) holds
( P _EQ_ Q iff [P,Q] in R_EllCur (a,b,p) )
let P, Q be Element of ProjCo (GF p); :: thesis: ( Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & Q in EC_SetProjCo (a,b,p) implies ( P _EQ_ Q iff [P,Q] in R_EllCur (a,b,p) ) )
assume A1: ( Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & Q in EC_SetProjCo (a,b,p) ) ; :: thesis: ( P _EQ_ Q iff [P,Q] in R_EllCur (a,b,p) )

hereby :: thesis: ( [P,Q] in R_EllCur (a,b,p) implies P _EQ_ Q )

assume P _EQ_ Q ; :: thesis: [P,Q] in R_EllCur (a,b,p)
then A2: [P,Q] in R_ProjCo p ;
[P,Q] in [:(EC_SetProjCo (a,b,p)),(EC_SetProjCo (a,b,p)):] by A1, ZFMISC_1:87;
hence [P,Q] in R_EllCur (a,b,p) by A2, XBOOLE_0:def 4; :: thesis: verum

end;

assume [P,Q] in R_EllCur (a,b,p) ; :: thesis: P _EQ_ Q
then [P,Q] in R_ProjCo p by XBOOLE_0:def 4;
hence P _EQ_ Q by Th46; :: thesis: verum