( k in NAT & dom (k |-> a) = Seg k ) by ORDINAL1:def 12;
hence len (k |-> a) = k by FINSEQ_1:def 3; :: according to CARD_1:def 7 :: thesis: verum