theorem Th12: :: AFINSQ_1:14

for k being Nat
for D being non empty set ex p being XFinSequence of D st len p = k