set F = multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #);
reconsider E = 0_EC (z,p) as Element of multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) ;
hence
multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) is unital
by GROUP_1:def 1; verum