theorem Th90: :: FINSEQ_2:92

for D being set
for z being FinSequence of D holds z is Element of (len z) -tuples_on D