consider f being FinSequence of D;
f in D * by Def11;
hence not D * is empty ; :: thesis: verum