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