set F = multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #);
P1: for h being Element of multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) holds
( h * (1_ multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #)) = h & (1_ multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #)) * h = h & ex g being Element of multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) st
( h * g = 1_ multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) & g * h = 1_ multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) ) )

proof

let h be Element of multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #); :: thesis:
thus ( h * (1_ multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #)) = h & (1_ multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #)) * h = h ) by GROUP_1:def 4; :: thesis:
reconsider h1 = h as Element of EC_SetAffCo (z,p) ;
reconsider g1 = (compell_AffCo (z,p)) . h1 as Element of EC_SetAffCo (z,p) ;
reconsider g = g1 as Element of multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) ;
set O = [0,1,0];
reconsider O = [0,1,0] as Element of multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) by ThAffCoZero;
take g ; :: thesis:
thus h * g = 0_EC (z,p) by ThAddCompAffCo
.= 1_ multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) by GP0 ; :: thesis:
thus g * h = (addell_AffCo (z,p)) . (h1,g1) by ThCommutativeAffCo
.= 0_EC (z,p) by ThAddCompAffCo
.= 1_ multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) by GP0 ; :: thesis:

end;

for x, y being Element of multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) holds x * y = y * x by BINOP_1:def 2;
hence ( multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) is commutative & multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) is Group-like & not multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) is empty ) by P1, GROUP_1:def 2, GROUP_1:def 12; :: thesis: