dom (Card A) = dom A by CARD_3:def 2;
hence Card A is Sequence-like by ORDINAL1:def 7; :: thesis: verum