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