theorem :: FINSEQ_1:57

for n being Nat holds card (Seg n) = n by Lm1, CARD_1:def 2;