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 Th33;
card (dom p) = card (len p) by A1, FINSEQ_1:55;
hence card (ProperPrefixes p) = len p by A2, CARD_1:5; :: thesis: verum