theorem Th95: :: FINSEQ_2:97

for D being non empty set
for z being Tuple of 1,D ex d being Element of D st z = <*d*>