:: deftheorem defines Z/Z* INT_7:def 4 :
for p being Prime holds Z/Z* p = multMagma(# (Segm0 p),(multint0 p) #);