let p be Prime; :: thesis:
A1: 1 < p by INT_2:def 5;
set Zp = multMagma(# (Segm0 p),(multint0 p) #);
A2: 1 in Segm p by A1, GR_CY_1:10;
not 1 in {0 } by TARSKI:def 1;
then 1 in (Segm p) \ {0 } by A2, XBOOLE_0:def 5;
then 1 in Segm0 p by A1, Def2;
then reconsider e = 1. (INT.Ring p) as Element of multMagma(# (Segm0 p),(multint0 p) #) by A1, INT_3:24;

A3: now

let h be Element of multMagma(# (Segm0 p),(multint0 p) #); :: thesis:
h in Segm0 p ;
then A4: h in (Segm p) \ {0 } by A1, 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 5 ; :: thesis:
thus e * h = (1_ (INT.Ring p)) * hp by Lm12
.= h by GROUP_1:def 5 ; :: thesis:
not h in {0 } by A4, XBOOLE_0:def 5;
then A5: hp <> 0 by TARSKI:def 1;
0 in Segm p by GR_CY_1:10;
then hp <> 0. (INT.Ring p) by A5, FUNCT_7:def 1;
then consider hpd being Element of (INT.Ring p) such that
A6: hpd * hp = 1. (INT.Ring p) by VECTSP_1:def 20;
hpd <> 0. (INT.Ring p) by A6, VECTSP_1:36;
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 A1, Def2;
A7: h * g = e by A6, Lm12;
g * h = e by A6, Lm12;
hence ex g being Element of multMagma(# (Segm0 p),(multint0 p) #) st
( h * g = e & g * h = e ) by A7; :: thesis:

end;

A8: multMagma(# (Segm0 p),(multint0 p) #) is associative

let x, y, z be Element of multMagma(# (Segm0 p),(multint0 p) #); :: according to GROUP_1:def 4 :: thesis:
x in Segm0 p ;
then x in (Segm p) \ {0 } by A1, 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 A1, 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 A1, Def2;
then reconsider z1 = z as Element of (INT.Ring p) by XBOOLE_0:def 5;
A9: x * y = x1 * y1 by Lm12;
A10: y * z = y1 * z1 by Lm12;
(x * y) * z = (x1 * y1) * z1 by A9, Lm12
.= x1 * (y1 * z1) by GROUP_1:def 4
.= x * (y * z) by A10, Lm12 ;
hence (x * y) * z = x * (y * z) ; :: thesis:

end;

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

let x, y be Element of multMagma(# (Segm0 p),(multint0 p) #); :: according to GROUP_1:def 16 :: thesis:
x in Segm0 p ;
then x in (Segm p) \ {0 } by A1, 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 A1, 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:

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 A3, A8, GROUP_1:def 3; :: thesis: