set f = the XFinSequence of D;
the XFinSequence of D in D ^omega by Def7;
hence not D ^omega is empty ; :: thesis: verum