theorem Th22: :: FINSEQ_2:24

for D being set
for D1 being Subset of D
for p being FinSequence of D1 holds p is FinSequence of D