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

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 . iend;

hence
(MergeSequence (p,q)) . i = p . i
; :: thesis: verumper cases
( i in dom p or not i in dom p )
;

end;

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;.= p . i by A1, FUNCOP_1:def 8 ;

:: thesis: verum

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;.= 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