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