let p be Prime; Z/Z* p = MultGroup (INT.Ring p)
A1:
0 in Segm p
by NAT_1:44;
then A2: (Segm p) \ {0} =
NonZero (INT.Ring p)
by SUBSET_1:def 8
.=
the carrier of (MultGroup (INT.Ring p))
by UNIROOTS:def 1
;
A3:
1 < p
by INT_2:def 4;
then A4: the multF of (Z/Z* p) =
(multint p) || ((Segm p) \ {0})
by INT_7:def 2
.=
the multF of (MultGroup (INT.Ring p))
by A2, UNIROOTS:def 1
;
0 = In (0,(Segm p))
by A1, SUBSET_1:def 8;
then the carrier of (Z/Z* p) =
NonZero (INT.Ring p)
by A3, INT_7:def 2
.=
the carrier of (MultGroup (INT.Ring p))
by UNIROOTS:def 1
;
hence
Z/Z* p = MultGroup (INT.Ring p)
by A4; verum