set G = INT.Group ;
reconsider e = 0 as Element of INT.Group by INT_1:def 2;
thus for h, g, f being Element of INT.Group holds (h * g) * f = h * (g * f) :: according to GROUP_1:def 3 :: thesis: INT.Group is Group-like
proof
let h, g, f be Element of INT.Group; :: thesis: (h * g) * f = h * (g * f)
reconsider A = h, B = g, C = f as Integer ;
A1: g * f = B + C by BINOP_2:def 20;
h * g = A + B by BINOP_2:def 20;
hence (h * g) * f = (A + B) + C by BINOP_2:def 20
.= A + (B + C)
.= h * (g * f) by A1, BINOP_2:def 20 ;
:: thesis: verum
end;
take e ; :: according to GROUP_1:def 2 :: thesis: for b1 being Element of the carrier of INT.Group holds
( b1 * e = b1 & e * b1 = b1 & ex b2 being Element of the carrier of INT.Group st
( b1 * b2 = e & b2 * b1 = e ) )
let h be Element of INT.Group; :: thesis: ( h * e = h & e * h = h & ex b1 being Element of the carrier of INT.Group st
( h * b1 = e & b1 * h = e ) )
reconsider A = h as Integer ;
- A in INT by INT_1:def 2;
then reconsider g = - A as Element of INT.Group ;
thus h * e = A + 0 by BINOP_2:def 20
.= h ; :: thesis: ( e * h = h & ex b1 being Element of the carrier of INT.Group st
( h * b1 = e & b1 * h = e ) )
thus e * h = 0 + A by BINOP_2:def 20
.= h ; :: thesis: ex b1 being Element of the carrier of INT.Group st
( h * b1 = e & b1 * h = e )
take g ; :: thesis: ( h * g = e & g * h = e )
thus h * g = A + (- A) by BINOP_2:def 20
.= e ; :: thesis: g * h = e
thus g * h = (- A) + A by BINOP_2:def 20
.= e ; :: thesis: verum