let X be set ; :: thesis: for x being Subset of X
for q being FinSequence of BOOLEAN holds len (MergeSequence (<*x*>,q)) = 1
let x be Subset of X; :: thesis: for q being FinSequence of BOOLEAN holds len (MergeSequence (<*x*>,q)) = 1
let q be FinSequence of BOOLEAN ; :: thesis: len (MergeSequence (<*x*>,q)) = 1
thus len (MergeSequence (<*x*>,q)) = len <*x*> by Def1
.= 1 by FINSEQ_1:39 ; :: thesis: verum