theorem Th19: :: AFINSQ_1:21

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