let n be non zero Nat; :: 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 ; :: thesis: verum