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

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