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