( k in NAT & dom (k |-> a) = Seg k ) by FUNCOP_1:19, ORDINAL1:def 13;
hence len (k |-> a) = k by FINSEQ_1:def 3; :: according to FINSEQ_1:def 18 :: thesis: verum