F . (Q,R) in EC_SetProjCo ((z `1),(z `2),p) ;
hence F . (Q,R) is Element of EC_SetProjCo ((z `1),(z `2),p) ; :: thesis: verum