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 :: thesis: (MergeSequence (p,q)) . i = p . i
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 ;
:: 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
.= p . i by ;
:: thesis: verum
end;
end;
end;
hence (MergeSequence (p,q)) . i = p . i ; :: thesis: verum