let n be non zero natural number ; :: thesis: card (INT.Group n) = n
multMagma(# (Segm n),(addint n) #) = INT.Group n by GR_CY_1:def 5;
hence card (INT.Group n) = n by CARD_1:def 2; :: thesis: verum