theorem :: FINSEQ_1:55

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