theorem Th2: :: YELLOW15:5

for X being set
for p being FinSequence of bool X
for q being FinSequence of BOOLEAN
for i being Nat st q . i = TRUE holds
(MergeSequence (p,q)) . i = p . i