let X be set ; :: thesis: for p being FinSequence of bool X

for q being FinSequence of BOOLEAN holds dom (MergeSequence (p,q)) = dom p

let p be FinSequence of bool X; :: thesis: for q being FinSequence of BOOLEAN holds dom (MergeSequence (p,q)) = dom p

let q be FinSequence of BOOLEAN ; :: thesis: dom (MergeSequence (p,q)) = dom p

thus dom (MergeSequence (p,q)) = Seg (len (MergeSequence (p,q))) by FINSEQ_1:def 3

.= Seg (len p) by Def1

.= dom p by FINSEQ_1:def 3 ; :: thesis: verum

for q being FinSequence of BOOLEAN holds dom (MergeSequence (p,q)) = dom p

let p be FinSequence of bool X; :: thesis: for q being FinSequence of BOOLEAN holds dom (MergeSequence (p,q)) = dom p

let q be FinSequence of BOOLEAN ; :: thesis: dom (MergeSequence (p,q)) = dom p

thus dom (MergeSequence (p,q)) = Seg (len (MergeSequence (p,q))) by FINSEQ_1:def 3

.= Seg (len p) by Def1

.= dom p by FINSEQ_1:def 3 ; :: thesis: verum