theorem Th10: :: FINSEQ_2:12

for p being FinSequence
for D being set st ( for i being Nat st i in dom p holds
p . i in D ) holds
p is FinSequence of D