the carrier of (D *+^+<0>) = D * by Th61;
hence the carrier of (D *+^+<0>) is FinSequence-membered ; :: thesis: verum