reconsider O = [0,1,0] as Element of EC_SetAffCo (z,p) by ThAffCoZero;
P1: O is_a_unity_wrt addell_AffCo (z,p) by ThUnityAffCo;
for P, Q being Element of EC_SetAffCo (z,p) holds (addell_AffCo (z,p)) . (P,Q) = (addell_AffCo (z,p)) . (Q,P) by ThCommutativeAffCo;
hence ( not addell_AffCo (z,p) is empty & addell_AffCo (z,p) is commutative & addell_AffCo (z,p) is having_a_unity ) by P1, BINOP_1:def 2, SETWISEO:def 2; :: thesis: verum