let X be set ; 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; for q being FinSequence of BOOLEAN holds len (MergeSequence (<*x,y*>,q)) = 2
let q be FinSequence of BOOLEAN ; len (MergeSequence (<*x,y*>,q)) = 2
thus len (MergeSequence (<*x,y*>,q)) =
len <*x,y*>
by Def1
.=
2
by FINSEQ_1:44
; verum