theorem Th21: :: FINSEQ_1:21

for p, q being FinSequence holds p = (p ^ q) | (dom p)