let A be included_in_Seg set ; :: thesis: len (Sgm A) = card A
A1: dom (Sgm A) = Seg (len (Sgm A)) by FINSEQ_1:def 3;
A2: card (Seg (len (Sgm A))) = len (Sgm A) by FINSEQ_1:57;
A4: rng (Sgm A) = A by FINSEQ_1:def 14;
Seg (len (Sgm A)),A are_equipotent by A1, A4;
hence len (Sgm A) = card A by A2, CARD_1:5; :: thesis: verum