theorem Th22: :: FINSEQ_3:22

for p, q being FinSequence
for x being object st x in dom p holds
x in dom (p ^ q)