theorem Th87: :: FINSEQ_2:89

for D being set holds D * is FinSequenceSet of D