:: deftheorem defines Z/Z GROUP_14:def 1 :
for n being natural Number holds Z/Z n = addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #);