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