let p be Prime; Z/Z* p = MultGroup (INT.Ring p)
A1:
0 in Segm p
by NAT_1:45;
then A2: (Segm p) \ {0 } =
NonZero (INT.Ring p)
by FUNCT_7:def 1
.=
the carrier of (MultGroup (INT.Ring p))
by UNIROOTS:def 1
;
A3:
1 < p
by INT_2:def 5;
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, FUNCT_7:def 1;
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