let p be Prime; :: thesis: for a, b being Element of (GF p)
for P being Element of ProjCo (GF p) holds
( P is_on_curve EC_WEqProjCo (a,b,p) iff P is Element of EC_SetProjCo (a,b,p) )
let a, b be Element of (GF p); :: thesis: for P being Element of ProjCo (GF p) holds
( P is_on_curve EC_WEqProjCo (a,b,p) iff P is Element of EC_SetProjCo (a,b,p) )
let P be Element of ProjCo (GF p); :: thesis: ( P is_on_curve EC_WEqProjCo (a,b,p) iff P is Element of EC_SetProjCo (a,b,p) )

hereby :: thesis: ( P is Element of EC_SetProjCo (a,b,p) implies P is_on_curve EC_WEqProjCo (a,b,p) )

assume P is_on_curve EC_WEqProjCo (a,b,p) ; :: thesis: P is Element of EC_SetProjCo (a,b,p)
then P in { Q where Q is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . Q = 0. (GF p) } ;
hence P is Element of EC_SetProjCo (a,b,p) by EC_PF_1:def 9; :: thesis: verum

end;

assume P is Element of EC_SetProjCo (a,b,p) ; :: thesis: P is_on_curve EC_WEqProjCo (a,b,p)
then P in EC_SetProjCo (a,b,p) ;
then P in { Q where Q is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . Q = 0. (GF p) } by EC_PF_1:def 9;
then ex Q being Element of ProjCo (GF p) st
( P = Q & (EC_WEqProjCo (a,b,p)) . Q = 0. (GF p) ) ;
hence P is_on_curve EC_WEqProjCo (a,b,p) ; :: thesis: verum