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

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 ; :: 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 ; :: 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, SUBSET_1:def 8;
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;
then hpd <> 0 ;
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

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