let p be Prime; :: thesis: for a, b being Element of (GF p) holds [0,1,0] is Element of EC_SetProjCo (a,b,p)
let a, b be Element of (GF p); :: thesis: [0,1,0] is Element of EC_SetProjCo (a,b,p)
( [0,1,0] is Element of ProjCo (GF p) & (EC_WEqProjCo (a,b,p)) . [0,1,0] = 0. (GF p) ) by Lm5;
then [0,1,0] in { P where P is Element of ProjCo (GF p) : (EC_WEqProjCo (a,b,p)) . P = 0. (GF p) } ;
hence [0,1,0] is Element of EC_SetProjCo (a,b,p) ; :: thesis: verum