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