theorem Th54: :: AFINSQ_1:57

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