set G = multMagma(# INT ,addint #);
thus for h, g, f being Element of multMagma(# INT ,addint #) holds (h * g) * f = h * (g * f) :: according to GROUP_1:def 4 :: thesis: multMagma(# INT ,addint #) is Group-like

proof

let h, g, f be Element of multMagma(# INT ,addint #); :: thesis: (h * g) * f = h * (g * f)
reconsider A = h, B = g, C = f as Integer ;
A1: h * g = A + B by Th14;
A2: g * f = B + C by Th14;
thus (h * g) * f = (A + B) + C by A1, Th14
.= A + (B + C)
.= h * (g * f) by A2, Th14 ; :: thesis: verum

end;

reconsider e = 0 as Element of multMagma(# INT ,addint #) by INT_1:def 2;
take e ; :: according to GROUP_1:def 3 :: thesis: for b₁ being Element of the carrier of multMagma(# INT ,addint #) holds
( b₁ * e = b₁ & e * b₁ = b₁ & ex b₂ being Element of the carrier of multMagma(# INT ,addint #) st
( b₁ * b₂ = e & b₂ * b₁ = e ) )
let h be Element of multMagma(# INT ,addint #); :: thesis: ( h * e = h & e * h = h & ex b₁ being Element of the carrier of multMagma(# INT ,addint #) st
( h * b₁ = e & b₁ * h = e ) )
reconsider A = h as Integer ;
thus h * e = A + 0 by Th14
.= h ; :: thesis: ( e * h = h & ex b₁ being Element of the carrier of multMagma(# INT ,addint #) st
( h * b₁ = e & b₁ * h = e ) )
thus e * h = 0 + A by Th14
.= h ; :: thesis: ex b₁ being Element of the carrier of multMagma(# INT ,addint #) st
( h * b₁ = e & b₁ * h = e )
reconsider g = - A as Element of multMagma(# INT ,addint #) by INT_1:def 2;
take g ; :: thesis: ( h * g = e & g * h = e )
thus h * g = A + (- A) by Th14
.= e ; :: thesis: g * h = e
thus g * h = (- A) + A by Th14
.= e ; :: thesis: verum