set f = the FinSequence of D;
the FinSequence of D in D * by Def11;
hence not D * is empty ; :: thesis: verum