dom (Card F) = dom F by CARD_3:def 2
.= Seg (len F) by FINSEQ_1:def 3 ;
hence Card F is FinSequence-like by FINSEQ_1:def 2; :: thesis: verum