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:56 ; :: thesis: verum