theorem Th13: :: FINSEQ_2:15

for i being natural Number
for p, q being FinSequence st i in dom p holds
i in dom (p ^ q)