consider p being Element of n -tuples_on {{} };
take p ; :: thesis: len p = n
thus len p = n by FINSEQ_2:109; :: thesis: verum