let p be FinSubsequence; :: thesis: card p = len (Seq p)
A1: ex k being Nat st dom p c= Seg k by FINSEQ_1:def 12;
A2: Seq p = p * (Sgm (dom p)) by FINSEQ_1:def 14;
A3: rng (Sgm (dom p)) = dom p by FINSEQ_1:71;
then A4: dom (Seq p) = dom (Sgm (dom p)) by A2, RELAT_1:46;
Sgm (dom p) is one-to-one by A1, FINSEQ_3:99;
then rng (Sgm (dom p)), dom (Sgm (dom p)) are_equipotent by WELLORD2:def 4;
then A5: card (dom p) = card (dom (Sgm (dom p))) by A3, CARD_1:21;
card (dom p) = card p by CARD_1:104;
hence card p = len (Seq p) by A4, A5, CARD_1:104; :: thesis: verum