let n be non zero Nat; :: thesis: the carrier of (INT.Group n) = Segm n
thus the carrier of (INT.Group n) = the carrier of multMagma(# (Segm n),(addint n) #) by GR_CY_1:def 5
.= Segm n ; :: thesis: verum