theorem :: FINSEQ_2:91

for D being non empty set
for D9 being Subset of D
for S being FinSequenceSet of D9 holds S is FinSequenceSet of D