theorem Th26: :: FINSEQ_1:26

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