let p be FinSequence; :: thesis: card (ProperPrefixes p) = len p
A1: dom p = Seg (len p) by FINSEQ_1:def 3;
( dom p is finite & ProperPrefixes p, dom p are_equipotent ) by Th67;
then ( card (dom p) = card (len p) & ProperPrefixes p is finite & card (ProperPrefixes p) = card (dom p) ) by A1, CARD_1:21, FINSEQ_1:76;
hence card (ProperPrefixes p) = len p ; :: thesis: verum