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)) #) ;

now :: thesis: for h being Element of multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) holds
( h * E = h & E * h = h )

let h be Element of multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #); :: thesis: ( h * E = h & E * h = h )
reconsider h1 = h as Element of EC_SetAffCo (z,p) ;
X1: 0_EC (z,p) is_a_unity_wrt addell_AffCo (z,p) by ThUnityAffCo;
hence h * E = h by BINOP_1:def 6, BINOP_1:def 7; :: thesis: E * h = h
thus E * h = h by X1, BINOP_1:def 5, BINOP_1:def 7; :: thesis: verum

end;

hence multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) is unital by GROUP_1:def 1; :: thesis: verum