theorem Th4: :: AFINSQ_2:4

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