theorem Th1: :: YELLOW15:4

for X being set
for p being FinSequence of bool X
for q being FinSequence of BOOLEAN holds dom (MergeSequence (p,q)) = dom p