let p be Prime; :: thesis: 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; :: thesis: verum

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; :: thesis: verum