consider m being Nat such that
B0: 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;
Z0: ( 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 {{}} by TARSKI:def 1;
then reconsider xx = the Element of (m + 1) -tuples_on X as Element of (X *) \ {{}} by Z0, XBOOLE_0:def 5;
take xx ; :: thesis: xx is n -element
thus xx is n -element by B0; :: thesis: verum