theorem Th10: :: AFINSQ_1:11

for k being Nat
for p being XFinSequence st k < len p holds
dom (p | k) = k