for p being Prime holds Z/Z* p = MultGroup (INT.Ring p)