let n be natural number ; :: thesis: ( n > 0 implies card (INT.Group n) = n )
assume A1: n > 0 ; :: thesis: card (INT.Group n) = n
set G = INT.Group n;
A2: multMagma(# (Segm n),(addint n) #) = INT.Group n by A1, GR_CY_1:def 6;
reconsider k = n as Element of NAT by ORDINAL1:def 13;
A3: Segm k is finite ;
then reconsider G = INT.Group n as finite Group by A2;

now

reconsider B = Segm n as finite set by A3;
take B = B; :: thesis: ( B = the carrier of G & n = card B )
thus B = the carrier of G by A2; :: thesis: n = card B
card B = card k by CARD_1:def 12;
hence n = card B by CARD_1:def 5; :: thesis: verum

end;

hence card (INT.Group n) = n ; :: thesis: verum