F . P in EC_SetAffCo (z,p) ;
hence F . P is Element of EC_SetAffCo (z,p) ; :: thesis: verum