let X be 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)
let p be 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 q be FinSequence of BOOLEAN ; for i being Nat st i in dom p & q . i = FALSE holds
(MergeSequence (p,q)) . i = X \ (p . i)
let i be Nat; ( 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
; (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
; verum