let n be natural number ; :: thesis: ( n > 0 implies card (INT.Group n) = n )
assume n > 0 ; :: thesis: card (INT.Group n) = n
then multMagma(# (Segm n),(addint n) #) = INT.Group n by GR_CY_1:def 6;
hence card (INT.Group n) = n by CARD_1:def 5; :: thesis: verum