let n be natural non zero number ; :: thesis: ( multMagma(# (Segm n),(addint n) #) is associative & multMagma(# (Segm n),(addint n) #) is Group-like )
set G = multMagma(# (Segm n),(addint n) #);
reconsider e = 0 as Element of multMagma(# (Segm n),(addint n) #) by NAT_1:45;
thus for h, g, f being Element of multMagma(# (Segm n),(addint n) #) holds (h * g) * f = h * (g * f) :: according to GROUP_1:def 4 :: thesis: multMagma(# (Segm n),(addint n) #) is Group-like

proof

let h, g, f be Element of multMagma(# (Segm n),(addint n) #); :: thesis: (h * g) * f = h * (g * f)
reconsider A = h, B = g, C = f as Element of Segm n ;
A1: g * f = (B + C) mod n by Def5;
h * g = (A + B) mod n by Def5;
hence (h * g) * f = (((A + B) mod n) + C) mod n by Def5
.= ((A + B) + C) mod n by NAT_D:22
.= (A + (B + C)) mod n
.= (A + ((B + C) mod n)) mod n by NAT_D:22
.= h * (g * f) by A1, Def5 ;
:: thesis: verum

end;

take e ; :: according to GROUP_1:def 3 :: thesis: for b₁ being Element of the carrier of multMagma(# (Segm n),(addint n) #) holds
( b₁ * e = b₁ & e * b₁ = b₁ & ex b₂ being Element of the carrier of multMagma(# (Segm n),(addint n) #) st
( b₁ * b₂ = e & b₂ * b₁ = e ) )
let h be Element of multMagma(# (Segm n),(addint n) #); :: thesis: ( h * e = h & e * h = h & ex b₁ being Element of the carrier of multMagma(# (Segm n),(addint n) #) st
( h * b₁ = e & b₁ * h = e ) )
reconsider A = h as Element of Segm n ;
reconsider A = A as Element of NAT ;
A2: A < n by NAT_1:45;
then consider p being Nat such that
A3: n = A + p by NAT_1:10;
thus h * e = (A + 0) mod n by Def5
.= h by A2, NAT_D:24 ; :: thesis: ( e * h = h & ex b₁ being Element of the carrier of multMagma(# (Segm n),(addint n) #) st
( h * b₁ = e & b₁ * h = e ) )
thus e * h = (0 + A) mod n by Def5
.= h by A2, NAT_D:24 ; :: thesis: ex b₁ being Element of the carrier of multMagma(# (Segm n),(addint n) #) st
( h * b₁ = e & b₁ * h = e )
p mod n < n by NAT_D:1;
then reconsider g = p mod n as Element of multMagma(# (Segm n),(addint n) #) by NAT_1:45;
reconsider B = g as Element of Segm n ;
take g ; :: thesis: ( h * g = e & g * h = e )
A4: p <= n by A3, NAT_1:12;
thus h * g = e :: thesis: g * h = e

proof

per cases ( p = n or p < n ) by A4, XXREAL_0:1;

suppose A5: p = n ; :: thesis: h * g = e

h * g = (A + B) mod n by Def5
.= (0 * n) mod n by A3, A5, NAT_D:25
.= e by NAT_D:13 ;
hence h * g = e ; :: thesis: verum

end;

suppose A6: p < n ; :: thesis: h * g = e

h * g = (A + B) mod n by Def5
.= n mod n by A3, A6, NAT_D:24
.= e by NAT_D:25 ;
hence h * g = e ; :: thesis: verum

end;

end;

end;

thus g * h = e :: thesis: verum

proof

per cases ( p = n or p < n ) by A4, XXREAL_0:1;

suppose p = n ; :: thesis: g * h = e

then g * h = ((n mod n) + 0) mod n by A3, Def5
.= (0 * n) mod n by NAT_D:25
.= e by NAT_D:13 ;
hence g * h = e ; :: thesis: verum

end;

suppose A7: p < n ; :: thesis: g * h = e

g * h = (A + B) mod n by Def5
.= n mod n by A3, A7, NAT_D:24
.= e by NAT_D:25 ;
hence g * h = e ; :: thesis: verum

end;

end;

end;