theorem :: AFINSQ_1:63

for D being set
for n being Nat
for r being set st r in D holds
n --> r is XFinSequence of D ;