let p be FinSequence; :: thesis: len (disjoin p) = len p
dom (disjoin p) = dom p by CARD_3:def 3;
hence len (disjoin p) = len p by Th27; :: thesis: verum