consider f being XFinSequence of ;
f in D ^omega by Def8;
hence not D ^omega is empty ; :: thesis: verum