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:50;
then A4: dom (Seq p) = dom (Sgm (dom p)) by A2, RELAT_1:27;
Sgm (dom p) is one-to-one by A1, Th90;
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:5;
card (dom p) = card p by CARD_1:62;
hence card p = len (Seq p) by A4, A5, CARD_1:62; :: thesis: verum