consider m being Nat such that
A1: n = m + 1 by NAT_1:6;
set x = the Element of (m + 1) -tuples_on X;
reconsider mm = m + 1 as Element of NAT by ORDINAL1:def 12;
A2: ( the Element of (m + 1) -tuples_on X in mm -tuples_on X & mm -tuples_on X c= X * ) by FINSEQ_2:134;
not the Element of (m + 1) -tuples_on X in {{}} ;
then reconsider xx = the Element of (m + 1) -tuples_on X as Element of (X *) \ {{}} by A2, XBOOLE_0:def 5;
take xx ; :: thesis: xx is n -element
thus xx is n -element by A1; :: thesis: verum