:: deftheorem Def1 defines MergeSequence YELLOW15:def 1 :
for X being set
for p being FinSequence of bool X
for q being FinSequence of BOOLEAN
for b₄ being FinSequence of bool X holds
( b₄ = MergeSequence (p,q) iff ( len b₄ = len p & ( for i being Nat st i in dom p holds
b₄ . i = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i))) ) ) );