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