theorem Th3: :: YELLOW15:6

for X being set
for p being FinSequence of bool X
for q being FinSequence of BOOLEAN
for i being Nat st i in dom p & q . i = FALSE holds
(MergeSequence (p,q)) . i = X \ (p . i)