the one-to-one FinSequence of D in D ** by Def2;
hence not D ** is empty ; :: thesis: verum