let X be set ; :: thesis: 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)

let p be FinSequence of bool X; :: thesis: 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)

let q be FinSequence of BOOLEAN ; :: thesis: for i being Nat st i in dom p & q . i = FALSE holds

(MergeSequence (p,q)) . i = X \ (p . i)

let i be Nat; :: thesis: ( i in dom p & q . i = FALSE implies (MergeSequence (p,q)) . i = X \ (p . i) )

assume that

A1: i in dom p and

A2: q . i = FALSE ; :: thesis: (MergeSequence (p,q)) . i = X \ (p . i)

thus (MergeSequence (p,q)) . i = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i))) by A1, Def1

.= X \ (p . i) by A2, FUNCOP_1:def 8 ; :: thesis: verum

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)

let p be FinSequence of bool X; :: thesis: 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)

let q be FinSequence of BOOLEAN ; :: thesis: for i being Nat st i in dom p & q . i = FALSE holds

(MergeSequence (p,q)) . i = X \ (p . i)

let i be Nat; :: thesis: ( i in dom p & q . i = FALSE implies (MergeSequence (p,q)) . i = X \ (p . i) )

assume that

A1: i in dom p and

A2: q . i = FALSE ; :: thesis: (MergeSequence (p,q)) . i = X \ (p . i)

thus (MergeSequence (p,q)) . i = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i))) by A1, Def1

.= X \ (p . i) by A2, FUNCOP_1:def 8 ; :: thesis: verum