the n -element XFinSequence of D in n -xtuples_of D by Def5;
hence not n -xtuples_of D is empty ; :: thesis: verum