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