theorem :: FINSEQ_2:117

for i being natural Number
for D being non empty set
for z being Tuple of i + 1,D ex t being Element of i -tuples_on D ex d being Element of D st z = t ^ <*d*>