let p be Prime; :: thesis: ( multMagma(# (Segm0 p),(multint0 p) #) is associative & multMagma(# (Segm0 p),(multint0 p) #) is commutative & multMagma(# (Segm0 p),(multint0 p) #) is Group-like )
set Zp = multMagma(# (Segm0 p),(multint0 p) #);
A1: not 1 in {0} by TARSKI:def 1;
A2: 1 < p by INT_2:def 4;
then 1 in Segm p by NAT_1:44;
then 1 in (Segm p) \ {0} by A1, XBOOLE_0:def 5;
then 1 in Segm0 p by A2, Def2;
then reconsider e = 1. (INT.Ring p) as Element of multMagma(# (Segm0 p),(multint0 p) #) by A2, INT_3:14;
A3: multMagma(# (Segm0 p),(multint0 p) #) is associative

proof

let x, y, z be Element of multMagma(# (Segm0 p),(multint0 p) #); :: according to GROUP_1:def 3 :: thesis: (x * y) * z = x * (y * z)
x in Segm0 p ;
then x in (Segm p) \ {0} by A2, Def2;
then reconsider x1 = x as Element of (INT.Ring p) by XBOOLE_0:def 5;
y in Segm0 p ;
then y in (Segm p) \ {0} by A2, Def2;
then reconsider y1 = y as Element of (INT.Ring p) by XBOOLE_0:def 5;
z in Segm0 p ;
then z in (Segm p) \ {0} by A2, Def2;
then reconsider z1 = z as Element of (INT.Ring p) by XBOOLE_0:def 5;
A4: y * z = y1 * z1 by Lm12;
x * y = x1 * y1 by Lm12;
then (x * y) * z = (x1 * y1) * z1 by Lm12
.= x1 * (y1 * z1) by GROUP_1:def 3
.= x * (y * z) by A4, Lm12 ;
hence (x * y) * z = x * (y * z) ; :: thesis: verum

end;

A5: now

let h be Element of multMagma(# (Segm0 p),(multint0 p) #); :: thesis: ( h * e = h & e * h = h & ex g being Element of multMagma(# (Segm0 p),(multint0 p) #) st
( h * g = e & g * h = e ) )
h in Segm0 p ;
then A6: h in (Segm p) \ {0} by A2, Def2;
then reconsider hp = h as Element of (INT.Ring p) by XBOOLE_0:def 5;
thus h * e = hp * (1_ (INT.Ring p)) by Lm12
.= h by GROUP_1:def 4 ; :: thesis: ( e * h = h & ex g being Element of multMagma(# (Segm0 p),(multint0 p) #) st
( h * g = e & g * h = e ) )
thus e * h = (1_ (INT.Ring p)) * hp by Lm12
.= h by GROUP_1:def 4 ; :: thesis: ex g being Element of multMagma(# (Segm0 p),(multint0 p) #) st
( h * g = e & g * h = e )
not h in {0} by A6, XBOOLE_0:def 5;
then A7: hp <> 0 by TARSKI:def 1;
0 in Segm p by NAT_1:44;
then hp <> 0. (INT.Ring p) by A7, FUNCT_7:def 1;
then consider hpd being Element of (INT.Ring p) such that
A8: hpd * hp = 1. (INT.Ring p) by VECTSP_1:def 9;
hpd <> 0. (INT.Ring p) by A8, VECTSP_1:6;
then hpd <> 0 by FUNCT_7:def 1;
then not hpd in {0} by TARSKI:def 1;
then hpd in (Segm p) \ {0} by XBOOLE_0:def 5;
then reconsider g = hpd as Element of multMagma(# (Segm0 p),(multint0 p) #) by A2, Def2;
A9: g * h = e by A8, Lm12;
h * g = e by A8, Lm12;
hence ex g being Element of multMagma(# (Segm0 p),(multint0 p) #) st
( h * g = e & g * h = e ) by A9; :: thesis: verum

end;

multMagma(# (Segm0 p),(multint0 p) #) is commutative

proof

let x, y be Element of multMagma(# (Segm0 p),(multint0 p) #); :: according to GROUP_1:def 12 :: thesis: x * y = y * x
x in Segm0 p ;
then x in (Segm p) \ {0} by A2, Def2;
then reconsider x1 = x as Element of (INT.Ring p) by XBOOLE_0:def 5;
y in Segm0 p ;
then y in (Segm p) \ {0} by A2, Def2;
then reconsider y1 = y as Element of (INT.Ring p) by XBOOLE_0:def 5;
x * y = x1 * y1 by Lm12
.= y * x by Lm12 ;
hence x * y = y * x ; :: thesis: verum

end;

hence ( multMagma(# (Segm0 p),(multint0 p) #) is associative & multMagma(# (Segm0 p),(multint0 p) #) is commutative & multMagma(# (Segm0 p),(multint0 p) #) is Group-like ) by A5, A3, GROUP_1:def 2; :: thesis: verum