let X be set ; :: thesis: 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
let p be FinSequence of bool X; :: thesis: for q being FinSequence of BOOLEAN
for i being Nat st q . i = TRUE holds
(MergeSequence (p,q)) . i = p . i
let q be FinSequence of BOOLEAN ; :: thesis: for i being Nat st q . i = TRUE holds
(MergeSequence (p,q)) . i = p . i
let i be Nat; :: thesis: ( q . i = TRUE implies (MergeSequence (p,q)) . i = p . i )
assume A1: q . i = TRUE ; :: thesis: (MergeSequence (p,q)) . i = p . i

now

per cases ( i in dom p or not i in dom p ) ;

suppose i in dom p ; :: thesis: (MergeSequence (p,q)) . i = p . i

hence (MergeSequence (p,q)) . i = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i))) by Def1
.= p . i by A1, FUNCOP_1:def 8 ;
:: thesis: verum

end;

suppose A2: not i in dom p ; :: thesis: (MergeSequence (p,q)) . i = p . i

dom p = Seg (len p) by FINSEQ_1:def 3
.= Seg (len (MergeSequence (p,q))) by Def1
.= dom (MergeSequence (p,q)) by FINSEQ_1:def 3 ;
hence (MergeSequence (p,q)) . i = {} by A2, FUNCT_1:def 2
.= p . i by A2, FUNCT_1:def 2 ;
:: thesis: verum

end;

end;

end;

hence (MergeSequence (p,q)) . i = p . i ; :: thesis: verum