theorem Th20: :: AFINSQ_1:22

for x being object
for p, q being XFinSequence st x in dom q holds
ex k being Nat st
( k = x & (len p) + k in dom (p ^ q) )